Rules with ∀
Just as with our propositional logic operators, there will be two inference rules for each of our predicate logic quanitifiers – an “introduction rule and an “elimination” rule.
In this section, we will see the two inference rules for the universal (∀) quantifier.
For all elimination
For all elimination allows us to take a claim that uses a universal quantifier – a statement about ALL individuals in a domain – and make the same statement about a specific individual in the domain. After all, if the statement is true for ALL individuals, then it follows that it should be true for a particular individual. We can formalize the rule as follows:
∀ ((x: T) => P(x))
AllE[T]: 
P(v) where v is a particular individual in the domain (i.e, v has type T)
Here is a simple example showing the syntax of the AllE[T]
rule. It shows that given the premises: All humans are mortal and Socrates is a human, that we can prove that Socrates is mortal:
( ∀ ((x: T) => (isHuman(x) → isMortal(x))),
isHuman(Socrates)
)
⊢
(
isMortal(Socrates)
)
Proof(
1 ( ∀ ((x: T) => (isHuman(x) → isMortal(x))) ) by Premise,
2 ( isHuman(Socrates) ) by Premise,
3 ( isHuman(Socrates) → isMortal(Socrates) ) by AllE[T](1),
4 ( isMortal(Socrates) ) by ImplyE(3, 2)
)
We can read the justification AllE[T](1)
as: “for all elimination of the for all statement on line 1.
While our AllE[T]
justification does not mention the particular individual that was plugged in to the for all statement (Socrates, in this case), it is required that whatever individual we plug in has already been show to be of type T
. This is done by accepting the individual as a parameter of type T
to the proof function. The full proof function would look like this:
@pure def socMortal[T](isHuman: T => B @pure, isMortal: T => B @pure, Socrates: T): Unit = {
Deduce (
(
∀ ((x: T) => (isHuman(x) → isMortal(x))),
isHuman(Socrates)
)
⊢
(
isMortal(Socrates)
)
Proof(
1 ( ∀ ((x: T) => (isHuman(x) → isMortal(x))) ) by Premise,
2 ( isHuman(Socrates) ) by Premise,
3 ( isHuman(Socrates) → isMortal(Socrates) ) by AllE[T](1),
4 ( isMortal(Socrates) ) by ImplyE(3, 2)
)
)
}
In similar examples of AllE[T]
, it is assumed that the named individual was accepted as a parameter of type T
to the proof function.
For all introduction
If we can show that a property of the form P(a)
holds for an arbitrary member a
of a domain, then we can use for all introduction to conclude that the property must hold for ALL individuals in the domain – i.e., that ∀ x P(x)
(which we write in Logika as ∀ ((x: T) => P(x))
). We can formalize the rule as follows:
Let ( (a: T) => SubProof(
...
P(a)
)),
AllI[T] : 
∀ ((x: T) => P(x))
Here is a simple example showing the syntax of the AllI[T]
rule: “Everyone is healthy; everyone is happy. Therefore, everyone is both healthy and happy.”:
(
∀((x: T) => isHealthy(x)), ∀((y: T) => isHappy(y))
)
⊢
(
∀((z: T) => isHealthy(z) ∧ isHappy(z))
)
Proof (
1 ( ∀((x: T) => isHealthy(x)) ) by Premise,
2 ( ∀((y: T) => isHappy(y)) ) by Premise,
3 Let ((a: T) => SubProof(
4 ( isHealthy(a) ) by AllE[T](1),
5 ( isHappy(a) ) by AllE[T](2),
6 ( isHealthy(a) ∧ isHappy(a) ) by AndI(4, 5)
)),
7 ( ∀((z: T) => isHealthy(z) ∧ isHappy(z)) ) by AllI[T](3)
)
If we wish to introduce a for all statement, the pattern is:

Open a subproof where you introduce an arbitrary/fresh individual in the domain with “Let” (in the example above, we used
a
). It MUST be a name that we have not used elsewhere in the proof. The idea is that your individual could have been anyone/anything in the domain. 
When you introduce the individual with “Let” and then open the subproof, you do NOT include a justification on that line

If you have other for all statements available within the scope of the subproof, then it is often useful to use
AllE[T]
to plug your fresh individual into them. After all, if those statements are true for ALL individuals, then they are also true for your fresh individual. 
If you are trying to prove something of the form
∀ ((x: T) => P(x))
, then you need to reachP(a)
by the end of the subproof. You need to show that your goal for all statement holds for your fresh individual. In our case, we wished to prove∀((z: T) => isHealthy(z) ∧ isHappy(z))
, so we reachedisHealthy(a) ∧ isHappy(a)
by the end of the subproof. 
After the subproof, you can use
∀i
to introduce a forall statement for your last claim in the subproof – that since the individual could have been anyone, then the proposition holds for ALL individuals. The∀i
justification needs the line number of the subproof. 
When you use
AllI[T]
, it does not matter what variable you introduce into the for all statement. In the example above, we introduced∀((z: T)
– but that was only to match the goal conclusion in the proof. We could have instead introduced∀((x: T)
,∀((y: T)
,∀((people T)
, etc. We would use whatever variable we chose in the rest of that proposition – i.e.,∀((z: T) => isHealthy(z) ∧ isHappy(z))
, or∀((people: T) => isHealthy(people) ∧ isHappy(people))
, etc.
Examples
In this section, we will look at additional proofs involving the universal quantifier.
Example 1
Suppose we wish to prove that, given the following premises in the domain of people:
 All students have a phone and/or a laptop
 Everyone is a student
Then we can conclude:
 Everyone has a phone and/or a laptop
First, we identify the following predicates:
isStudent(x)
 whether person x is a studenthasPhone(x)
 whether person x has a phonehasLaptop(x)
= whether person x has a laptop
Then, we can translate our premises and goal conclusion to predicate logic:
 All students have a phone and/or a laptop translates to:
∀ x (isStudent(x) → hasPhone(x) ∨ hasLaptop(x))
 Everyone is a student translates to:
∀ x isStudent(x)
 Everyone has a phone and/or a laptop translates to:
∀ x (hasPhone(x) ∨ hasLaptop(x))
We need to prove the following sequent (where we rewrite the above predicate logic statements in our Logika format):
(
∀((x: T) => (isStudent(x) → hasPhone(x) ∨ hasLaptop(x))),
∀((x: T) => isStudent(x))
)
⊢
(
∀((y: T) => (hasPhone(y) ∨ hasLaptop(y)))
)
As with our previous example, we see that we are trying to prove a forall statement (∀((y: T) => (hasPhone(y) ∨ hasLaptop(y)))
). This means we will need to open a subproof and introduce a fresh individual – perhaps bob
. By the end of the subproof, we must show that our goal forall statement holds for that individual – that hasPhone(bob) ∨ hasLaptop(bob)
. We start the proof as follows:
(
∀((x: T) => (isStudent(x) → hasPhone(x) ∨ hasLaptop(x))),
∀((x: T) => isStudent(x))
)
⊢
(
∀((y: T) => (hasPhone(y) ∨ hasLaptop(y)))
)
Proof (
1 ( ∀((x: T) => (isStudent(x) → hasPhone(x) ∨ hasLaptop(x))) ) by Premise,
2 ( ∀((x: T) => isStudent(x)) ) by Premise,
3 Let ( (bob: T) => SubProof(
//goal: hasPhone(bob) ∨ hasLaptop(bob)
)),
//use AllI to conclude ∀((y: T) => (hasPhone(y) ∨ hasLaptop(y)))
)
We have two available forall statements within the subproof – ∀((x: T) => (isStudent(x) → hasPhone(x) ∨ hasLaptop(x)))
and ∀((x: T) => isStudent(x))
. Since those propositions hold for all individuals, they also hold for bob
. We use AllE[T]
to plug in bob
to those two propositions:
(
∀((x: T) => (isStudent(x) → hasPhone(x) ∨ hasLaptop(x))),
∀((x: T) => isStudent(x))
)
⊢
(
∀((y: T) => (hasPhone(y) ∨ hasLaptop(y)))
)
Proof (
1 ( ∀((x: T) => (isStudent(x) → hasPhone(x) ∨ hasLaptop(x))) ) by Premise,
2 ( ∀((x: T) => isStudent(x)) ) by Premise,
3 Let ( (bob: T) => SubProof(
4 ( isStudent(bob) → hasPhone(bob) ∨ hasLaptop(bob) ) by AllET(1),
5 ( isStudent(bob) ) by AllE[T](2),
//goal: hasPhone(bob) ∨ hasLaptop(bob)
)),
//use AllI to conclude ∀((y: T) => (hasPhone(y) ∨ hasLaptop(y)))
)
Line 5 is an implies statement the form p → q
, and line 6 is a statement of the form p
. Thus we can use →e
to conclude hasPhone(bob) ∨ hasLaptop(bob)
(the “q” in that statement) – which is exactly what we needed to end the subproof. All that remains is to apply our AlI
rule after the subproof. Here is the completed proof:
(
∀((x: T) => (isStudent(x) → hasPhone(x) ∨ hasLaptop(x))),
∀((x: T) => isStudent(x))
)
⊢
(
∀((y: T) => (hasPhone(y) ∨ hasLaptop(y)))
)
Proof (
1 ( ∀((x: T) => (isStudent(x) → hasPhone(x) ∨ hasLaptop(x))) ) by Premise,
2 ( ∀((x: T) => isStudent(x)) ) by Premise,
3 Let ( (bob: T) => SubProof(
4 ( isStudent(bob) → hasPhone(bob) ∨ hasLaptop(bob) ) by AllET(1),
5 ( isStudent(bob) ) by AllE[T](2),
6 ( hasPhone(bob) ∨ hasLaptop(bob) ) by ImplyE(4, 5)
)),
7 ( ∀((y: T) => (hasPhone(y) ∨ hasLaptop(y))) ) by AllI[T](3)
)
Example 2
Next, suppose we wish to prove the following sequent:
(
∀((x: T) => (S(x) → Pz(x))),
∀((x: T) => (Pz(x) → D(x))),
∀((x: T) => ¬D(x))
)
⊢
(
∀((x: T) => ¬S(x))
)
We again see that the toplevel operator of what we are trying to prove is a universal quantifier. We use our strategy to open a subproof with a fresh individual (maybe a
), and plug that individual into any available forall statements. Since we wish to prove ∀((x: T) => ¬S(x))
, then we will want to reach ¬S(a)
by the end of the subproof. Here is a sketch:
(
∀((x: T) => (S(x) → Pz(x))),
∀((x: T) => (Pz(x) → D(x))),
∀((x: T) => ¬D(x))
)
⊢
(
∀((x: T) => ¬S(x))
)
Proof(
1 ( ∀((x: T) => (S(x) → Pz(x))) ) by Premise,
2 ( ∀((x: T) => (Pz(x) → D(x)) ) by Premise,
3 ( ∀((x: T) => ¬D(x)) ) by Premise,
4 Let ((a: T) => SubProof (
5 ( S(a) → Pz(a) ) by AllE[T](1),
6 ( Pz(a) → D(a) ) by AllE[T](2),
7 ( ¬D(a) ) by AllE[T](3),
//goal: ¬S(a)
)),
//use AllI[T] to conclude ∀((x: T) => ¬S(x))
)
Now, we see that our goal is to reach ¬S(a)
by the end of the subproof – so we need to prove something whose toplevel operator is a NOT. We recall that we have a strategy to prove NOT(something) from propositional logic – we open a subproof, assuming something (S(a)
, in our case), try to get a contradiction, and use negation introduction after the subproof to conclude NOT (something) (¬S(a)
for us). Here is the strategy:
(
∀((x: T) => (S(x) → Pz(x))),
∀((x: T) => (Pz(x) → D(x))),
∀((x: T) => ¬D(x))
)
⊢
(
∀((x: T) => ¬S(x))
)
Proof(
1 ( ∀((x: T) => (S(x) → Pz(x))) ) by Premise,
2 ( ∀((x: T) => (Pz(x) → D(x)) ) by Premise,
3 ( ∀((x: T) => ¬D(x)) ) by Premise,
4 Let ((a: T) => SubProof(
5 ( S(a) → Pz(a) ) by AllE[T](1),
6 ( Pz(a) → D(a) ) by AllE[T](2),
7 ( ¬D(a) ) by AllE[T](3),
8 SubProof(
10 Assume( S(a) ),
//goal: contradiction
),
//use NegI to conclude ¬S(a)
//goal: ¬S(a)
)),
//use AllI[T] to conclude ∀((x: T) => ¬S(x))
)
We can complete the proof as follows:
(
∀((x: T) => (S(x) → Pz(x))),
∀((x: T) => (Pz(x) → D(x))),
∀((x: T) => ¬D(x))
)
⊢
(
∀((x: T) => ¬S(x))
)
Proof(
1 ( ∀((x: T) => (S(x) → Pz(x))) ) by Premise,
2 ( ∀((x: T) => (Pz(x) → D(x)) ) by Premise,
3 ( ∀((x: T) => ¬D(x)) ) by Premise,
4 Let ((a: T) => SubProof(
5 ( S(a) → Pz(a) ) by AllE[T](1),
6 ( Pz(a) → D(a) ) by AllE[T](2),
7 ( ¬D(a) ) by AllE[T](3),
8 SubProof(
10 Assume( S(a) ),
11 ( Pz(a) ) by ImplyE(5, 10),
12 ( D(a) ) by ImplyE(6, 11),
13 ( F ) by NegE(12, 7)
//goal: contradiction
),
//use ¬i to conclude ¬S(a)
14 ( ¬S(a) ) by NegI(8)
//goal: ¬S(a)
)),
//use AllI[T] to conclude ∀((x: T) => ¬S(x))
15 ( ∀((x: T) => ¬S(x)) ) by AllI[T](4)
)