12/30/20
Skills to be acquired in this tutorial:
To learn about functional terms and two new Rules of Inference II (Identity Introduction) and IE (Identity Elimination).
Why this is useful:
Reasoning with identity is vital for mathematics, philosophy, and many other areas.
The Tutorial:
An aside on functions and some universal abilities of human beings
Consider the statement that Allison’s only brother’s wife’s only sister is her very best friend. There is barely a person on Earth who does not understand what this means. Most everyone also knows full well what it is for the assertion to be true.
The example is interesting because it illustrates instantiation of the use and understanding of high level concepts which seem to be universal. These include partial functions, function application or compositions, constructions, types, and the distinction between a construction and that which the construction constructs.
Being an only brother, wife, only sister, etc. are all partial functions. Functions carry one thing to another, and partial functions are functions which might not defined everywhere. Being a only brother, wife, only sister, etc. are partial functions with types-- they are defined on humans (or, perhaps, animals) and definitely not on cars or tables or trees.
'Construction' is a term coined by Pavel Tichy ([1986]). It means 'way of arriving at, usually by means of functions and function abstractions, compositions and applications', so the expression 'Allison only brother’s wife’s only sister' refers to a construction. Further, suppose that all the various partial functions are properly defined, with suitable uniqueness for the arguments, so that the construction via the (only) brother function etc. picks someone, say Flora, and, supposing the assertion to be true, the other construction, via the very best friend partial function, also constructs Flora; we are all very well aware that the two constructions and that which they construct, Flora, are three different things. [Many of us would also realize, with reflection, that there is universal widespread systematic ambiguity between constructions and that which they construct. But that is another story, not entered into here.] So,
Allison brother’s wife’s sister is a construction, and Flora is what it constructs.
[Allison's] very best friend is a construction, and Flora is what it constructs.
And what Allison’s brother’s wife’s sister is her very best friend is telling us is that the two different constructions construct the same thing (and notice, in particular, that it is not telling us that Flora is Flora).
Back to the main theme
The word 'terms' in logic means 'names' and thus far we have met two kinds of terms: constants (or proper names), and variables.
These are not the only names there are. In English consider 'the father of Betty' -- now, this is not a statement, it does not say something true or false, rather it is a construction which names an individual. It takes Betty and what we might call the 'father of' function and uses the two of those to name an individual. Similarly in mathematics, the expression 7 + 2 does not assert something true or false, rather it is a construction which names a number (which also happens to have the name 9).
The logic we are studying, so called 'First order logic', can accommodate these fancy terms, and it does so by means of 'functional terms'.
Here is a characterization of our syntax for functional terms
- any constant is a functional term.
- any lower case letter followed by ( followed by any number of functional terms followed by ) is a functional term.
- and these are all the functional terms there are.
For example, a, b, c, f(a), g(b), g(ac), h(g(c)b) ... are all functional terms.
To symbolize, say,
'The father of Betty is kind'
we choose, say, f(x) to represent the 'father of x' function, b to represent Betty, and Kx to represent the predicate 'x is kind' and the whole lot becomes:
Kf(b)
This same process is extended to arguments. So the argument
Everything is kind.
Therefore,
Betty's father is kind.
could be
(∀x)Kx ∴ Kf(b)
And, of course, this is valid and the derivation is simple just using Universal Instantiation.
Functional terms often appear in identities. For example
Allison’s brother’s wife’s sister is her very best friend.
might be symbolized
s(w(b(a)))=f(a)
where a=Allison, b(x)= is the brother of x, s(x)= is the sister of x, w(x)= is the wife of x, f(x)= is the very best friend of x,
Functional terms have an 'arity', which, roughly, is the number of arguments they apply to. Remember with predicates you can have one place predicates like Fx, and two place predicates, or relations, like Txy (and three place...). So too with functional terms. The 'father of' function is of arity one-- it expects one term as an argument. In mathematics there are plenty of functions of higher arity. For example, the plus function usually expects two arguments, so 'plus x y' might be represented p(xy).
Actually, there is another small issue that comes up here. The way we write functional terms is to write the function first, followed by the arguments. In math, a fair few functions are 'infix', that is to say they are written between their arguments instead of before them-- mathematicians generally write (1 + 2) not +(1 2).
[For your information, Deriver can be configured to do formal arithmetic (which is too advanced for us just at the moment) and if so configured it is familiar with the following conventions:-
It knows about + ('plus') and . (times) and ' (successor of), and 0,1, 2. + and . are infix and successor is postfix (it comes after its argument) and 0,1, 2 are just the constants 0, 1, 2. 'successor of' just means the number plus one (so the successor of 3 is 4 etc.) Deriver can read an expression like the following K(0+0') and what this says is that '0 plus the successor of 0 has the property K'.
None of these extended capabilities are of immediate interest to us.]
Our Predicate Logic is also extended by having two new rules, one for introducing and the other eliminating identity. In Deriver, you will find these rules under the Advanced Menu.
The Identity Introduction rule, labeled '=I',
allows you to bring in
<term>=<same term>
for any term that you like.
So, to give several examples, you can have
a=a
f(hj)=f(hj)
g(b(c))=g(b(c))
all justified by the rule =I.
The Identity Elimination rule, labeled '=E',
is the one that allows you to substitute identical things, one for another. And you use the elimination rule with one identity, say s=t, and one other formula, say F-- you are allowed to substitute chosen occurrences of s in F with t (and chosen occurrences of t in F with s). Often the formula F is itself a statement of identity-- perhaps one formula is a=b and the other b=c; in these cases there are lots of opportunities for substituting. Here are several examples (lines 4,5,6, and 8).
In one strict form of the rule, substitutions are permitted only within atomic formulas (or their negations). But this can lead to long derivations, with taking a compound formula apart, making a substitution, then putting it back together again.
To simplify issues here we permit substitutions into compound formulas, so, for example a=b can be used to substitute into (∀x)(Kx⊃Fa) .But now we have to go careful with free, bound, free for and capturing (which you are familiar with from Tutorial 24 in Easy Deriver https://softoption.us/node/541). So, there is one restriction. No variable that occurs in the terms of the identity, s or t, say, can be bound in the <formula> you are substituting into. So, with f(x)=g(y,z) and (∀m)(Ff(x)m)∧(∃z)(g(y,z)=a) you are not allowed to substitute because the variable z occurs in the identity and is bound in the formula.
Exercise to accompany Identity Tutorial 2 .
Exercise 1(of 3)
Formalize and then derive the following valid argument.
a=Ann
f(x)= father of X
Px= X is a friendly personEvery friendly person's father is friendly.
Ann is a friendly person.
Therefore,
Ann's father is friendly.
[Answer is (d) below]
Exercise 2(of 3)
Proofs
Derive the following
a) Gab, a=b ∴ Gaa∧Gbb
b) a=b,b=c ∴ a=c∧c=a
c) (∀x)Kx ∴ Kf(b)
d) (∀x)(Fx⊃ Ff(x)),Fa ∴ Ff(a)
Exercise 3(of 3)
Proofs
Identity has some general properties, namely, i) everything is identical to itself, ii) if a = b, then b = a, and iii) if a=b and b=c, then a=c. These are known as reflexivity, symmetry, and transitivity, and they can be enshrined into three theorems (which you can prove).
Theorem 1
∴ (∀x)(x=x)
Theorem 2
∴ (∀x)(∀y)((x=y)⊃(y=x))
Theorem 3
∴ (∀x)(∀y)(∀z)(((x=y)∧(y=z))⊃(x=z))
If you decide to use the web application for the exercises you can launch it from here Deriver [Gentzen] — username 'logic' password 'logic'. Then either copy and paste the above formulas into the Journal or use the Deriver File Menu to Open Web Page with this address https://softoption.us/test/Deriver/CombinedTutorialsGentzen.html .
Preferences
You will need to set some Preferences for this.
- set identity to true (and that will give you the identity rules)
- set firstOrder to true (to get first order theories)
- and you can check that the parser is set to gentzen.