As with Propositional Logic, we can demonstrate logical entailment in Relational Logic by writing proofs. As with Propositional Logic, it is possible to show that a set of Relational Logic premises logically entails a Relational Logic conclusion if and only if there is a finite proof of the conclusion from the premises. Moreover, it is possible to find such proofs in a finite time.
The Fitch system for Relational Logic is an extension of the Fitch system for Propositional Logic. In addition to the logical rules of inference we have already seen, there are a few new rules of inference (described in the next section) - rules of inference for universally quantified sentences, rules of inference for existentially quantified sentences, and a new type of rule called Domain Closure.
Note that the Fitch system described here works only for premises and conclusions that are closed sentences. This is not a significant limitation, since every open sentence is logically equivalent to a closed sentence in which the free variables have been universally quantified.
Use the arrow keys to navigate. Press the escape key to toggle all / one.