Variable declarations in natural deduction (Q861825)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
scientific article; zbMATH DE number 5121376
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Variable declarations in natural deduction |
scientific article; zbMATH DE number 5121376 |
Statements
Variable declarations in natural deduction (English)
0 references
2 February 2007
0 references
The version of natural deduction for the first-order logic without equality proposed here (call it D) seems to be very similar to the ordinary (Gentzen-Prawitz) version of natural deduction (call it G) except for Fitch format. Every deduction in D is a deduction in G; every deduction in G becomes a deduction in D after inserting ``declare \(v\)'' before the first (uppermost) occurrence of the variable \(v\) in every branch. Most part of the paper consists of comments addressed mainly to readers having little experience with the use of variables in mathematics or programming.
0 references
natural deduction
0 references
variable proviso
0 references
0 references
0.8357824
0 references
0.83322483
0 references
0.82863927
0 references
0.82807505
0 references
0.8221233
0 references
