Fitch notation, also known as Fitch diagrams (named after
Frederic Fitch
Frederic Brenton Fitch (September 9, 1908, Greenwich, Connecticut – September 18, 1987, New Haven, Connecticut) was an American logician, a Sterling Professor at Yale University.
Education and career
At Yale, Fitch earned his B.A in 1931 and ...
), is a notational system for constructing
formal proof
In logic and mathematics, a formal proof or derivation is a finite sequence of sentences (called well-formed formulas in the case of a formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the seq ...
s used in
sentential logics and
predicate logics. Fitch-style proofs arrange the sequence of sentences that make up the proof into rows. A unique feature of Fitch notation is that the degree of indentation of each row conveys which assumptions are active for that step.
Example
Each row in a Fitch-style proof is either:
* an assumption or subproof assumption.
* a sentence justified by the citation of (1) a
rule of inference
In the philosophy of logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions). For example, the rule of ...
and (2) the prior line or lines of the proof that license that rule.
Introducing a new assumption increases the level of indentation, and begins a new vertical "scope" bar that continues to indent subsequent lines until the assumption is discharged. This mechanism immediately conveys which assumptions are active for any given line in the proof, without the assumptions needing to be rewritten on every line (as with sequent-style proofs).
The following example displays the main features of Fitch notation:
0 , __ ssumption, want P iff not not P1 , , __ P ssumption, want not not P2 , , , __ not P ssumption, for reductio3 , , , contradiction ontradiction introduction: 1, 24 , , not not P egation introduction: 2 ,
5 , , __ not not P ssumption, want P6 , , P egation elimination: 5 ,
7 , P iff not not P iconditional introduction: 1 - 4, 5 - 6
0. The null assumption, ''i.e.'', we are proving a
tautology
1. Our first subproof: we assume the l.h.s. to show the r.h.s. follows
2. A subsubproof: we are free to assume what we want. Here we aim for a
reductio ad absurdum
In logic, (Latin for "reduction to absurdity"), also known as (Latin for "argument to absurdity") or ''apagogical arguments'', is the form of argument that attempts to establish a claim by showing that the opposite scenario would lead to absu ...
3. We now have a contradiction
4. We are allowed to prefix the statement that "caused" the contradiction with a not
5. Our second subproof: we assume the r.h.s. to show the l.h.s. follows
6. We invoke the rule that allows us to remove an even number of nots from a statement prefix
7. From 1 to 4 we have shown if P then not not P, from 5 to 6 we have shown P if not not P; hence we are allowed to introduce the biconditional
See also
*
Natural deduction In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use ax ...
References
*
Frederic Brenton Fitch
Frederic Brenton Fitch (September 9, 1908, Greenwich, Connecticut – September 18, 1987, New Haven, Connecticut) was an American logician, a Sterling Professor at Yale University.
Education and career
At Yale, Fitch earned his B.A in 1931 and h ...
, ''Symbolic Logic: An introduction'', Ronald Press Co., 1952.
*
Jon Barwise
Kenneth Jon Barwise (; June 29, 1942 – March 5, 2000) was an American mathematician, philosopher and logician who proposed some fundamental revisions to the way that logic is understood and used.
Education and career
Born in Independence, ...
and
John Etchemendy
John W. Etchemendy (born 1952 in Reno, Nevada) is an American logician and philosopher who served as Stanford University's twelfth Provost. He succeeded John L. Hennessy to the post on September 1, 2000 and stepped down on January 31, 2017.
E ...
,
Language, Proof and Logic
Language, Proof and Logic is an educational software package, devised and written by Jon Barwise and John Etchemendy, geared to teaching formal logic through the use of a tight integration between a textbook (same name as the package) and four sof ...
br>
''1st edition as PDF'' Seven Bridges Press and CSLI, 1999.
External links
Fitch's Paradox of Knowability{{Webarchive, url=https://web.archive.org/web/20061002151420/http://logik.phl.univie.ac.at/%7Echris/gateway/formular-uk-fitch.html , date=2006-10-02
A Web implementation of Fitch proof system (propositional and first-order) at proofmod.mindconnect.ccThe Jape general-purpose proof assistant(see
Jape
Jape is a synonym for a practical joke.
Jape or JAPE may also refer to:
* Jape (band), an Irish electronic/rock band
* JAPE (linguistics), a transformation language widely used in natural language processing
* JAPE, an automated pun generator
* J ...
)
Resources for typesetting proofs in Fitch notation with LaTeX(see
LaTeX
Latex is an emulsion (stable dispersion) of polymer microparticles in water. Latexes are found in nature, but synthetic latexes are common as well.
In nature, latex is found as a milky fluid found in 10% of all flowering plants (angiosperms ...
)
FitchJS: An open source web app to construct proofs in Fitch notation (and export to LaTeX)Natural deduction proof editor and checker in Fitch notation
Philosophical logic
Logical calculi