10/8/09 Under construction
<constant> ::= (['0'-'9']) |'∅'| 'U'|'{ }'
<subscript> ::= ['₁'-'₉']
<functor> ::= ['a'-'v'](< subscript >)*
<variable> ::= ['w'-'z'](< subscript >)*
<term> ::=
12/13/09
(Many) sorted logic, with sorts or sort labels, is very similar in concept and execution to the types and type labels just discussed (in fact, many texts use the two terms interchangeably). There is, though, a conceptual difference. It is that whereas both ordinary logic and logic with type labels use one (homogenous) domain or universe, sorted logic uses a (usually stratified, heterogenous) domain which consists of two or more sub-domains.
An example will help.
8/19/26
Type labels are one way to approach what seem to be different domains in use in the same reasoning. What we are going to do here is to tag the variables with a type to indicate that they are subject to a particular monadic (one-place) predicate applying to what they pick out. An example will help, say 'All men die' is symbolized
(∀x)(Mx⊃Dx)
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).