1/27/09 10 Software
To learn how to use the Universal and Existential Quantifiers in symbolizing propositions.
You may have derivations of your own that you wish to try. Just type, paste, or drag and drop, them into the panel, select your derivation, and click 'Start from selection'.
[Often copy-and-paste won't work directly from a Web Page; however, usually drag-and-drop will work!]
You will need to use the correct logical symbols. Here they are
F ∴ F ∧ G ∼ ∧ ∨ ⊃ ≡ ∀ ∃ ∴
Tutorial 6: Abelian Groups Tutorial 7: Boolean Algebra Tutorial 8: Linearly Ordered Sets Coming sometime!
Theorem 1
| 1 | x=x | =I | ||
| 2 | (∀x)(x=x) | 1 UG | ||
Theorem 2
1/17/20
1/17/20
[This is a film-- press the 'play' symbol.]
1/9/09
Your browser does not support the video tag.
-->
[What is shown below is a Video, with sound. Your computer should be able to run this. If you have external speakers, or similar, you may need to turn them on and turn the volume up.]
The video shows an older implementation (but it should convey the principles).
1/9/09
This shows the general technique for proving identities between sets.
1/10/09 13 Software
Some predicate logic proofs or derivations using Gentzen calculus. Try to prove them (click 'Derive It' off the Wizard Menu, if you want help).