Logika Predicate Logic Proof Syntax

We will use the following format in Logika to start a natural deduction proof for predicate logic. Each proof will be saved in a new file with a .sc (Scala) extension:

// #Sireum #Logika
//@Logika: --manual --background type

import org.sireum._
import org.sireum.justification._
import org.sireum.justification.natded.prop._
import org.sireum.justification.natded.pred._

@pure def ProofName[T](pred1: T => B @pure, pred2: T => B @pure, ..., indiv1: T, indiv2: T, ...): Unit = {
    Deduce(
        //@formatter:off
        (comma-separated list of premises with variable1, variable2, ...)  ⊢  (conclusion)
            Proof(
                //the actual proof steps go here
            )
        //@formatter:on
    )
}

Here, T is the type of elements in our domain. Usually, we will just use T to denote a generic type (much like generics in Java and C#), but occasionally we will use specific types like Z (which means “integer”). Next, pred1, pred2, etc. are the predicates for our proofs. The T => B means that they take an element in our domain as a parameter (which has type T) and return a boolean (which has type B). Finally, indiv1, indiv2, etc. are specific individuals within our domain, each of which have type T.

A proof function like the example above can have as many or few predicates and individuals as are needed for the proof.

As was the case with propositional logic, the examples in this chapter will omit the imports, proof function definition, deduce call, and formatter changes are omitted here for readability. We will start each example with the sequent followed by the Proof call.

For all statements in Logika

The syntax of a statement like ∀ x P(x) in Logika is a little different, since we must specify that each x is an element in our domain. When we are using Logika to do a predicate logic proof, we express ∀ x P(x) as:

∀ ((x: T) => P(x))

The above statement is saying, “for all x that are of the type T, P(x) is true”.

We can alternatively use curly braces instead of standard parentheses to surround our predicate:

∀ {(x: T) => P(x)}

Such statements can be a pain to type out manually, so there is a way to insert them using a template. If you right-click where you wish to write a predicate logic statement, you can select Slang->Insert Template->Forall. This will insert the statement:

∀((ID: TYPE) => CLAIM)

You can type your variable name (often x, y, etc.) in place of ID, the domain type (usually T) in place of TYPE, and your claim (with predicates and propositional logic operators) in place of CLAIM.

Finally, you can type the keyboard shortcut Ctrl+Shift+, A to insert a for all statement.

There exists statements in Logika

Statements with existential quantifiers like ∃ x P(x) must also be treated differently. When we are using Logika to do a predicate logic proof, we express ∃ x P(x) as:

∃ ((x: T) => P(x))

The above statement is saying, “there exists an x with type T where P(x) is true”.

We can alternatively use curly braces instead of standard parentheses to surround our predicate:

∃ {(x: T) => P(x)}

Such statements can be a pain to type out manually, so there is a way to insert them using a template. If you right-click where you wish to write a predicate logic statement, you can select Slang->Insert Template->Exists. This will insert the statement:

∃((ID: TYPE) => CLAIM)

You can type your variable name (often x, y, etc.) in place of ID, the domain type (usually T) in place of TYPE, and your claim (with predicates and propositional logic operators) in place of CLAIM.

Finally, you can type the keyboard shortcut Ctrl+Shift+, E to insert a there exists statement.

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 reach P(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 reached isHealthy(a) ∧ isHappy(a) by the end of the subproof.

• After the subproof, you can use ∀i to introduce a for-all 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 student
• hasPhone(x) - whether person x has a phone
• hasLaptop(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 for-all 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 for-all 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 for-all 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 top-level 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 for-all 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 top-level 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)
)

Rules with ∃

In this section, we will see the two inference rules for the existential (∃) quantifier.

Exists introduction

We can use the exists introduction rule, ExistsI[T], when we have a proposition of the form P(a) for an arbitrary member a of a domain. Since we found one individual where a proposition held, then we can also say that there exists an individual for which the proposition is true. We can formalize the rule as follows:

                   P(d)         where  d  is an individual of type T
ExistsI[T]: ---------------------
              ∃((x: T) => P(x))

Here is a simple example showing the syntax of the ExistsI[T] rule (where Socrates is a parameter of type T to our proof function):

(   isHuman(Socrates)   ) ⊢ (   ∃((x: T) => isHuman(x))  )
    
    Proof(
        1 (     isHuman(Socrates)       )   by Premise,
        2 (     ∃((x: T) => isHuman(x)) )   by ExistsI[T](1)
    )

When we use the ExistsI[T] rule to justify a claim like ∃((x: T) => P(x)), we include the line number of where the proposition held for a particular individual. In the proof above, we claim ∃((x: T) => isHuman(x)) with justification ExistsI[T](1) – line 1 corresponds to isHuman(Socrates), where our ∃((x: T) => isHuman(x)) proposition held for a particular individual. The full proof function, which shows how Socrates can be accepted as a parameter of type T, is here:

@pure def ExistsExample[T](isHuman: T => B @pure, Socrates: T): Unit = {
    Deduce(
        (   isHuman(Socrates)   ) ⊢ (   ∃((x: T) => isHuman(x))  )
    
        Proof(
            1 (     isHuman(Socrates)       )   by Premise,
            2 (     ∃((x: T) => isHuman(x)) )   by ExistsI[T](1)
        )
    )
}

Note that we can use the ExistsI[T] rule to introduce any variable, not just x. You can choose which variable to introduce based on the variables used in the conclusion. For example, the following proof is also valid:

(   isHuman(Socrates)   ) ⊢ (   ∃((z: T) => isHuman(z))  )
    
    Proof(
        1 (     isHuman(Socrates)       )   by Premise,
        2 (     ∃((z: T) => isHuman(z)) )   by ExistsI[T](1)
    )

Exists elimination

Since the ExistsI[T]-rule constructs propositions that begin with ∃, the ExistsE[T]-rule (exists elimination) disassembles propositions that begin with ∃.

Here is a quick example (where our domain is living things):

• All humans are mortal
• Someone is human
• Therefore, someone is mortal

We don’t know the name of the human, but it does not matter. Since ALL humans are mortal and SOMEONE is human, then our anonymous human must be mortal. The steps will go like this:

• Since “someone is human” and since we do not know his/her name, we will just make up our own name for them – “Jane”. So, we assume that “Jane is human”.

• We use the logic rules we already know to prove that “Jane is mortal”.

• Therefore, SOMEONE is mortal and their name does not matter.

This approach is coded into the last logic law, ExistsE[T] (exists elimination).

Suppose we have a premise of the form ∃((x: T) => P(x)). Since we do not know the name of the individual “hidden” behind the ∃(x: T), we make up a name for it, say a, and discuss what must follow from the assumption that P(a) holds true. Here is the formalization of the ExistsE[T] rule:

                                        Let ((a: T) => SubProof(          // where  a  is a new, fresh name
                                             Assume( P(a) ),              // a  MUST NOT appear in  Q
                ∃((x: T) => P(x))            ...
                                             Q         
                                        )),             
ExistsE[T]: ----------------------------------------------------
                     Q

That is, if we can deduce Q from P(a), and we do not mention a within Q, then it means Q can be deduced no matter what name the hidden individual has. So, Q follows from ∃((x: T) => P(x)).

We can work the previous example, with ExistsE[T]:

All humans are mortal
Someone is human
Therefore, someone is mortal

We make up the name, jane, for the human whose name we do not know:

    (
        ∀((h: T) => (isHuman(h) → isMortal(h))),
        ∃((x: T) => isHuman(x))
    )
⊢
    (
        ∃((y: T) => (isMortal(y)))
    )
Proof(
    1 (     ∀((h: T) => (isHuman(h) → isMortal(h)))     )   by Premise,
    2 (     ∃((x: T) => isHuman(x))                     )   by Premise,

    3 Let ( (jane: T) => SubProof (
        4 Assume(   isHuman(jane)                       ),
        5 (         isHuman(jane) → isMortal(jane)      )   by AllE[T](1),
        6 (         isMortal(jane)                      )   by ImplyE(5, 4)
    )),
    7 (     ∃((y: T) => (isMortal(y)))                  )   by ExistsE[T](2, 3)
)

Line 3 proposes the name jane for our subproof and line 4 makes the assumption isHuman(jane) (based on the premise ∃((x: T) => isHuman(x))). The subproof leads to Line 6, which says that someone is mortal. (We never learned the individual’s name!) Since Line 6 does not explicitly mention the made-up name, jane, we use Line 7 to repeat Line 6 – without knowing the name of the individual “hiding” inside Line 2, we made a subproof that proves the result, anyway. This is how ExistsE[T] works.

Note that when we use the ExistsE[T] rule as a justification we include first the line number of the there exists statement that we processed (by naming the hidden individual) in the previous subproof, and then the line number of that subproof. In the example above, we say ExistsE[T](2, 3) because line 2 includes the there-exists statement we processed (∃ ∃((x: T) => isHuman(x))) in the previous subproof and line 3 is the subproof.

When using ExistsE[T], the previous subproof must begin with introducing a name for a hidden individual in a there-exists statement and then immediately make an assumption that substitutes the name into the there exists statement. The last line in the subproof should contain NO mention of the chosen name. Whatever we claim on the last line in the subproof, we must claim EXACTLY the same thing immediately afterwards when we use the ExistsE[T] rule.

You are welcome to use any name for the hidden individual – not just jane or a. The only restriction is that you cannot have used the name anywhere else in the proof.

Examples

In this section, we will look at other proofs involving the existential quantifier.

Example 1

Suppose we wish to prove the following sequent:

(   ∃((x: T) => (Adult(x) ∨ Kid(x)))  ) ⊢ (   ∃((x: T) => Adult(x) )) ∨ ∃((x: T) => Kid(x)  )

We will begin as we did previously: by introducing an alias for our person that is either an adult or a kid (say, alice):

(   ∃((x: T) => (Adult(x) ∨ Kid(x)))  ) ⊢ (   ∃((x: T) => Adult(x) )) ∨ ∃((x: T) => Kid(x)  )

Proof(
    1 (     ∃((x: T) => (Adult(x) ∨ Kid(x)) )       )   by Premise,

    2 Let ( (alice: T) => SubProof(
        3 Assume(   Adult(alice) ∨ Kid(alice)       ),
        
        //goal: get to our conclusion, ∃( (x: T) => Adult(x) )) ∨ ∃( (x: T) => Kid(x)
    )),

    //use ExistsE[T] to restate our conclusion, since we know SOME such person is either an adult or kid
)

To finish our proof, we can use OR elimination on Adult(alice) ∨ Kid(alice), and then ExistsE[T] afterwards to restate our conclusion. Here is the completed proof:

(   ∃((x: T) => (Adult(x) ∨ Kid(x)))  ) ⊢ (   ∃((x: T) => Adult(x) )) ∨ ∃((x: T) => Kid(x)  )

Proof(
    1 (     ∃((x: T) => (Adult(x) ∨ Kid(x)) )                   )   by Premise,

    2 Let ( (alice: T) => SubProof(
        3 Assume(   Adult(alice) ∨ Kid(alice)                   ),

        4 SubProof(
            5 Assume (  Adult(alice)                            ),
            6 (     ∃((x: T) => Adult(x)                        )   by ExistsI[T](5),
            7 (     ∃((x: T) => Adult(x) ∨ ∃((x: T) => Kid(x)   )   by OrI1(6)
        ),
        8 SubProof(
            9 Assume (  Kid(alice)                              ),
            10 (    ∃((x: T) => Kid(x)                          )   by ExistsI[T](9),
            11 (    ∃((x: T) => Adult(x) ∨ ∃((x: T) => Kid(x)   )   by OrI2(10)
        ),
        12 (    ∃((x: T) => Adult(x) ∨ ∃((x: T) => Kid(x)       )   by OrE(3, 4, 8)
        
        //goal: get to our conclusion, ∃( (x: T) => Adult(x) )) ∨ ∃( (x: T) => Kid(x)
    )),
    //use ExistsE[T] to restate our conclusion, since we know SOME such person is either an adult or kid

    13 (        ∃((x: T) => Adult(x) ∨ ∃((x: T) => Kid(x)       )   by ExistsE[T](1, 2)
)

Example 2

Suppose we wish to prove the following (in the domain of living things):

• All bunnies are fluffy
• There is a fast bunny
• Therefore, there is a creature that is fast and fluffy

We can translate our premises and desired conclusion to predicate logic, and write the following sequent:

    (
        ∀((x: T) => (Bunny(x) → Fluffy(x))),
        ∃((x: T) => (Fast(x) & Bunny(x))) 
    )
⊢
    (
        ∃((x: T) => (Fast(x) & Fluffy(x)))
    )

Since we are trying to prove a claim about some individual, it makes sense that we would start the process of an ExistsE[T] subproof where we introduce an alias (thumper) for the fast bunny. We will try to reach the conclusion by the end of that subproof. Here is the setup:

    (
        ∀((x: T) => (Bunny(x) → Fluffy(x))),
        ∃((x: T) => (Fast(x) & Bunny(x))) 
    )
⊢
    (
        ∃((x: T) => (Fast(x) & Fluffy(x)))
    )
Proof(
    1 (     ∀((x: T) => (Bunny(x) → Fluffy(x)))     )   by Premise,
    2 (     ∃((x: T) => (Fast(x) & Bunny(x)))       )   by Premise,

    3 Let ( (thumper: T) => SubProof(
        4 Assume(   Fast(thumper) ∧ Bunny(thumper)  ),
        5 (         Fast(thumper)                   )   by AndE1(4),
        6 (         Bunny(thumper)                  )   by AndE2(4),

        //goal: ∃((x: T) => (Fast(x) & Fluffy(x)))
    )),

    //use ExistsE[T] to restate ∃((x: T) => (Fast(x) & Fluffy(x))), since we know there is SOME fast bunny
)

To finish our subproof, we see that we have a proposition about all creatures (∀((x: T) => (Bunny(x) → Fluffy(x)))) and that we are working with an individual creature (thumper). We can use AllE[T] to prove Bunny(thumper) → Fluffy(thumper). After that, we have a few more manipulations using propositional logic rules, our ExistsI[T] rule to transition our claim from being about our alias thumper to being about an unnamed individual, and then our ExistsE[T] rule to pull our final claim out of the subproof. Here is the completed proof:

    (
        ∀((x: T) => (Bunny(x) → Fluffy(x))),
        ∃((x: T) => (Fast(x) & Bunny(x))) 
    )
⊢
    (
        ∃((x: T) => (Fast(x) & Fluffy(x)))
    )
Proof(
    1 (     ∀((x: T) => (Bunny(x) → Fluffy(x)))         )   by Premise,
    2 (     ∃((x: T) => (Fast(x) & Bunny(x)))           )   by Premise,

    3 Let ( (thumper: T) => SubProof(
        4 Assume(   Fast(thumper) ∧ Bunny(thumper)      ),
        5 (         Fast(thumper)                       )   by AndE1(4),
        6 (         Bunny(thumper)                      )   by AndE2(4),
        7 (         Bunny(thumper) → Fluffy(thumper)    )   by AllE[T](1),
        8 (         Fluffy(thumper)                     )   by ImplyE(7, 6),
        9 (         Fast(thumper) ∧ Fluffy(thumper)     )   by AndI(5, 8),
        10 (        ∃((x: T) => (Fast(x) & Fluffy(x)))  )   by ExistsI[T](9)

        //goal: ∃((x: T) => (Fast(x) & Fluffy(x)))
    )),
    //use ExistsE[T] to restate ∃((x: T) => (Fast(x) & Fluffy(x))), since we know there is SOME fast bunny

    11 (    ∃((x: T) => (Fast(x) & Fluffy(x)))          )   by ExistsE[T](2, 3)
)

Nested Quantifiers

Our examples so far have included propositions with single quantifiers. This section will discuss how to prove sequents that use nested quantifers. We will see that the approach is the same as before, but that we must take caution to process the quantifiers in the correct order. Recall that quantifier precedence is from right to left (i.e., from the outside in), so that ∀ x ∀ y P(x, y) is equivalent to ∀ x (∀ y P(x, y)).

//<——————COME UP WITH DIFFERENT EXAMPLE 1!!!!!——————->

Example 1

Suppose we wish to prove the following sequent:

    (
        ∀((x: T) => ∀((y: T) => (P(x, y) → Q(x, y)))),
        ∀((x: T) => ∀((y: T) => P(x, y)))
    )
⊢
    (
        ∀((x: T) => ∀((y: T) => Q(x, y)))
    )

Since we wish to prove a for-all statement, ∀((x: T) => (SOMETHING), we know we must start with our for all introduction template:

    (
        ∀((x: T) => ∀((y: T) => (P(x, y) → Q(x, y)))),
        ∀((x: T) => ∀((y: T) => P(x, y)))
    )
⊢
    (
        ∀((x: T) => ∀((y: T) => Q(x, y)))
    )
Proof(
    1 (     ∀((x: T) => ∀((y: T) => (P(x, y) → Q(x, y))))       )   by Premise,
    2 (     ∀((x: T) => ∀((y: T) => P(x, y)))                   )   by Premise,
    
    3 Let (  (a: T)  => SubProof(

        //need: ∀((y: T) => Q(a, y))
    )),
    //want to use AllI[T] to conclude ∀((x: T) => ∀((y: T) => Q(x, y)))
)

But now we see that we want to prove ANOTHER for-all statement, ∀((y: T) => Q(a, y)). So we again use our for all introduction strategy in a nested subproof:

    (
        ∀((x: T) => ∀((y: T) => (P(x, y) → Q(x, y)))),
        ∀((x: T) => ∀((y: T) => P(x, y)))
    )
⊢
    (
        ∀((x: T) => ∀((y: T) => Q(x, y)))
    )
Proof(
    1 (     ∀((x: T) => ∀((y: T) => (P(x, y) → Q(x, y))))       )   by Premise,
    2 (     ∀((x: T) => ∀((y: T) => P(x, y)))                   )   by Premise,
    
    3 Let (  (a: T)  => SubProof(
        4 ( (b: T) => SubProof(

            //need: Q(a, b)
        )),
        //want to use AllI[T] to conclude ∀((y: T) => Q(a, y))

        //need: ∀((y: T) => Q(a, y))
    )),
    //want to use AllI[T] to conclude ∀((x: T) => ∀((y: T) => Q(x, y)))
)

Now, in subproof 4, we see that we must use AllE[T] on our both of our premises to work towards our goal of Q(a, b). We have two available individuals – a and b. When we use AllE[T], we must eliminate the OUTER (top-level) quantifier and its variable. In the case of the premise ∀((x: T) => ∀((y: T) => (P(x, y) → Q(x, y)))), we see that we must eliminate the ∀((x: T) ...). Since the x is the first parameter in Q(x, y), and since we are hoping to reach Q(a, b) by the end of subproof 4, we can see that we need to plug in the a for the x so that it will be in the desired position. We make a similar substitution with AllE[T] on our second premise:

    (
        ∀((x: T) => ∀((y: T) => (P(x, y) → Q(x, y)))),
        ∀((x: T) => ∀((y: T) => P(x, y)))
    )
⊢
    (
        ∀((x: T) => ∀((y: T) => Q(x, y)))
    )
Proof(
    1 (     ∀((x: T) => ∀((y: T) => (P(x, y) → Q(x, y))))       )   by Premise,
    2 (     ∀((x: T) => ∀((y: T) => P(x, y)))                   )   by Premise,
    
    3 Let (  (a: T)  => SubProof(
        4 ( (b: T) => SubProof(

            5 (     ∀(y: T) => (P(a, y) → Q(a, y)))             )   by AllE[T](1),
            6 (     ∀(y: T) => P(a, y)                          )   by AllE[T](2),

            //need: Q(a, b)
        )),
        //want to use AllI[T] to conclude ∀((y: T) => Q(a, y))

        //need: ∀((y: T) => Q(a, y))
    )),
    //want to use AllI[T] to conclude ∀((x: T) => ∀((y: T) => Q(x, y)))
)

Note that on line 5, we could NOT have used AllE[T] to eliminate the ∀(y: T) in ∀((x: T) => ∀((y: T) => (P(x, y) → Q(x, y)))) , as it was not the top-level operator.

Next, we apply AllE[T] again to our results on lines 5 and 6, this time plugging in b for y in both cases. This leaves us with P(a, b) → Q(a, b) and P(a, b). We can use implies elimination to reach our goal of Q(a, b), and then all that remains ais to use AllI[T] twice as planned to wrap up the two subproofs. Here is the completed proof:

    (
        ∀((x: T) => ∀((y: T) => (P(x, y) → Q(x, y)))),
        ∀((x: T) => ∀((y: T) => P(x, y)))
    )
⊢
    (
        ∀((x: T) => ∀((y: T) => Q(x, y)))
    )
Proof(
    1 (     ∀((x: T) => ∀((y: T) => (P(x, y) → Q(x, y))))       )   by Premise,
    2 (     ∀((x: T) => ∀((y: T) => P(x, y)))                   )   by Premise,
    
    3 Let (  (a: T)  => SubProof(
        4 ( (b: T) => SubProof(

            5 (     ∀(y: T) => (P(a, y) → Q(a, y))              )   by AllE[T](1),
            6 (     ∀(y: T) => P(a, y)                          )   by AllE[T](2),
            7 (     P(a, b) → Q(a, b)                           )   by AllE[T](5),
            8 (     P(a, b)                                     )   by ALlE[T](6),
            9 (     Q(a, b)                                     )   by ImplyE(7, 8)

            //need: Q(a, b)
        )),
        //want to use AllI[T] to conclude ∀((y: T) => Q(a, y))
        10 (    ∀((y: T) => Q(a, y))                            )   by AllI[T](4)

        //need: ∀((y: T) => Q(a, y))
    )),
    //want to use AllI[T] to conclude ∀((x: T) => ∀((y: T) => Q(x, y)))
    11 (    ∀((x: T) => ∀((y: T) => Q(x, y)))                   )   by AllI[T](3)
)

Example 2

Suppose we have the predicate IsBossOf(x, y) in the domain of people, which describes whether person x is the boss of person y. We wish to prove the following sequent:

    (
        ∃((x: T) => ∀((y: T) => IsBossOf(x, y)))
    )
⊢
    (
        ∀((y: T) => ∃((x: T) => IsBossOf(x, y)))
    )

You can read the premise as “There is a person that is everyone’s boss”. From this statement, we are trying to prove the conclusion: “All people have a boss”. Here is the completed proof:

    (
        ∃((x: T) => ∀((y: T) => IsBossOf(x, y)))
    )
⊢
    (
        ∀((y: T) => ∃((x: T) => IsBossOf(x, y)))
    )

Proof(
    1 (     ∃((x: T) => ∀((y: T) => IsBossOf(x, y)))            )   by Premise,

    2 Let ( (a: T) => SubProof(
        3 Assume(   ∀((y: T) => IsBossOf(a, y)                  )

        4 Let ( (b: T) => SubProof(
            5 (         IsBossOf(a, b)                          )   by AllE[T](3),
            6 (         ∃((x: T) => IsBossOf(x, b))             )   by ExistsI[T](5)
        )),
        7 (   ∀((y: T) => ∃((x: T) => IsBossOf(x, y)))          )   by AllI[T](4)
    )),
    8 (   ∀((y: T) => ∃((x: T) => IsBossOf(x, y)))              )  by ExistsE[T](1, 2)
)

In the above proof, we let a be our made-up name for the boss-of-everyone. So, we have the assumption that ∀((y: T) => IsBossOf(a, y)). Next, we let b be “anybody at all” who we might examine in the domain of people. The proof exposes that the boss of “anybody at all” in the domain must always be a. AllI[T] and then ExistsE[T] finish the proof.

Here is the proof worked again, with the subproofs swapped:

    (
        ∃((x: T) => ∀((y: T) => IsBossOf(x, y)))
    )
⊢
    (
        ∀((y: T) => ∃((x: T) => IsBossOf(x, y)))
    )

Proof(
    1 (     ∃((x: T) => ∀((y: T) => IsBossOf(x, y)))            )   by Premise,

    2 Let ( (b: T) => SubProof(

        3 Let ( (a: T) => SubProof(
            4 Assume(   ∀((y: T) => IsBossOf(a, y))             ),
            5 (         IsBossOf(a, b)                          )   by AllE[T](4),
            6 (         ∃((x: T) => IsBossOf(x, b))             )   by ExistsI[T](5)
        )),
        7 (       ∃((x: T) => IsBossOf(x, b))                   )   by ExistsE[T](1, 3)
    )),
    8 (   ∀((y: T) => ∃((x: T) => IsBossOf(x, y)))              )  by AllI[T](2)
)

Can we prove the converse? That is, if everyone has a boss, then there is one boss who is the boss of everyone? NO. We can try, but we get stuck:

    (
        ∀((y: T) => ∃((x: T) => IsBossOf(x, y)))
    )
⊢
    (
        ∃((x: T) => ∀((y: T) => IsBossOf(x, y)))
    )

Proof(
    1 (     ∀((y: T) => ∃((x: T) => IsBossOf(x, y)))            )   by Premise,

    2 Let ( (a: T) => SubProof(
        3 (     ∃((x: T) => IsBossOf(x, a))                     )   by AllE[T](1),
        
        4 Let ( (b: T) => SubProof(
            5 (     Assume (    IsBossOf(b, a)                  ),
        )),
        6 (     ∀((y: T) => IsBossOf(b, y))                     )   AllI[T](4),

        //STEP 6 IS INVALID -- we cannot refer to b after the end of the subproof
        //where it was introduced

    )),
    
    //...can't finish
)

We see that the “block structure” of the proofs warns us when we are making invalid deductions.

Equivalence

In Chapter 5, we saw DeMorgan’s laws for quantifiers – that if we have some domain, and if P(x) is a predicate for individuals in that domain, then the following statements are equivalent:

• ¬(∃ x P(x)) is equivalent to ∀ x ¬P(x)
• ¬(∀ x P(x)) is equivalent to ∃ x ¬P(x)

The process of proving that two predicate logic statements are equivalent is the same as it was in propositional logic – we must prove the second proposition using the first as a premise, and we must prove the first given the second as a premise.

Example - how to prove equivalence

For example, to prove that ¬(∃ x P(x)) is equivalent to ∀ x ¬P(x), we must prove the sequents:

    (
        ¬(∃((x: T) => P(x)))
    )
⊢
    (
        ∀((x: T) => ¬P(x))
    )

and

    (
        ∀((x: T) => ¬P(x))
    )
⊢
    (
        ¬(∃((x: T) => P(x)))
    )

We prove both directions below:

    (
        ¬(∃((x: T) => P(x)))
    )
⊢
    (
        ∀((x: T) => ¬P(x))
    )
Proof(
    1 (     ¬(∃((x: T) => P(x)))        ) by Premise,

    2 Let ( (a: T) => SubProof(

        3 SubProof(
            4 Assume (  P(a)  ),
            5 (     ∃((x: T) => P(x))   ) by ExistsI[T](3),
            6 (     F                   ) by NegE(4, 1)
        ),
        7 (     ¬P(a)                   ) by NegI(3)

    )),
    8 (  ∀((x: T) => ¬P(x))             ) by AllI[T](2)
)

And:

    (
        ∀((x: T) => ¬P(x))
    )
⊢
    (
        ¬(∃((x: T) => P(x)))
    )
Proof(
    1 (     ∀((x: T) => ¬P(x))          )   by Premise,

    2 SubProof(
        3 Assume (  ∃((x: T) => P(x))   ),

        4 Let ( (a: T) => SubProof(
            5 Assume (  P(a)  ),
            6 (     ¬P(a)               )   by AllE[T](1),
            7 (     F                   )   by NegE(5, 6),
        )),
        8 (     F                       )   By ExistsE[T](3, 4)
    
    ),
    9 (     ¬(∃((x: T) => P(x)))        )   by NegI(2)
)

More extensive list of equivalences

Here is a more extensive list of equivalences in predicate logic. The remaining proofs are left as exercises for the reader:

• ¬(∃ x P(x)) is equivalent to ∀ x ¬P(x)
• ¬(∀ x P(x)) is equivalent to ∃ x ¬P(x)
• ∀ x (P(x) → ¬Q(x)) is equivalent to ¬(∃ x P(x) ∧ Q(x))
• ∀ x ∀ y P(x, y) is equivalent to ∀ y ∀ x P(x, y)
• ∃ x ∃ y P(x, y) is equivalent to ∃ y ∃ x P(x, y)
• Q ∧ (∀ x P(x)) is equivalent to ∀ x (Q ∧ P(x)) (where x does not appear in Q)
• Q v (∀ x P(x)) is equivalent to ∀ x (Q V P(x)) (where x does not appear in Q)
• Q ∧ (∃ x P(x)) is equivalent to ∃ x (Q ∧ P(x)) (where x does not appear in Q)
• Q V (∃ x P(x)) is equivalent to ∃ x (Q V P(x)) (where x does not appear in Q)

Summary and Strategies

In this section, we summarize all available rules in propositional logic, and discuss strategies for approaching proofs.

Rules with universal quantifier (∀)

Rule summaries:

           ∀ ((x: T) => P(x))
AllE[T]:  ---------------------
                   P(v)     where v is a particular individual in the domain (i.e, v has type T)

            Let (   (a: T) => SubProof(
                ... 
                P(a)  
            )),
AllI[T] : -------------------------------
                 ∀ ((x: T) => P(x)) 

Rule syntax summaries:

( 
    ...
    r (     ∀ ((x: T) => P(x))      )   by SomeJustification,
    s (     P(v)                    )   by AllE[T](r),      //where v has been previously shown to have type T    
    ...
)

( 
    ...
    r Let (  (a: T) => SubProof(    //where a is a fresh, previously unused, individual
        ...
        t (     P(a)            )   by SomeJustification
    )),
    u (     ∀ ((x: T) => P(x))  )   by AllI[T](r),
)

Rules with existential quantifier (∃)

Rule summaries:

                   P(d)         where  d  is an individual of type T
ExistsI[T]: ---------------------
              ∃((x: T) => P(x))

                                        Let ((a: T) => SubProof(          // where  a  is a new, fresh name
                                             Assume( P(a) ),              // a  MUST NOT appear in  Q
                ∃((x: T) => P(x))            ...
                                             Q         
                                        )),             
ExistsE[T]: ----------------------------------------------------
                     Q

Rule syntax summaries:

(
    ...
    r (     P(d)                )   by SomeJustification,   //where d has been shown to have type T
    s (     ∃((x: T) => P(x))   )   by ExistsI[T](r),
    ...
)

(
    ...
    b (     ∃((x: T) => P(x))       )   by SomeJustification,
    c Let ( (a: T) => SubProof(     //where a is a previously unused individual
        d Assume(  P(a)  ),
        ...
        f (     Q                   )   by SomeJustification    //where a does NOT appear in Q
    )),
    g (     Q                       )   by ExistsE[T](b, c),
    ...
)

Reminder: propositional logic rules are still available

When doing proofs in predicate logic, remember that all the deduction rules from propositional logic are still available. You will often want to use the same strategies we saw there – not introduction to prove a NOT, implies introduction to create an implies statement, OR elimination to process an OR statement, etc.

However, keep in mind that propositional logic rules can only be used on claims without quantifiers as their top-level operator. For example, if we have the statement ∀ ( x: T) => (S(x) ∧ Pz(x)) ), then we cannot use AndE – the top-level operator is a universal quantifier, and the ∧ statement is “bound up” in that quantifier. We would only be able to use AndE after we had used AllE[T] to eliminate the quantifier.

Strategies

1. Write down all premises first. Can you extract anything from the premises?

   • If you have a for-all statement and an available individual, use AndE[T] to plug that individual into the for-all statement.
   • If you have p∧q, use AndE1 to extract p by itself and then AndE2 to extract q by itself.
   • If you have p →: q and p, use ImplyE to get q.
   • If you have p and ¬p, use NegE to claim a contradiction, F.

2. Look at the top-level operator of what you are trying to prove.

   • Are you trying to prove something of the form ∀ ((x: T) => P(x))?

     • Use AllI[T]. Open a subproof, introduce a fresh a, and get to P(a) by the end of the subproof. After the subproof, use AllI[T] to conclude ∀ ((x: T) => P(x)).

   • Are you trying to prove something of the form ∃((x: T) => P(x))?

     • You will often have another there-exists (∃) statement available as a premise or previous claim. Open a subproof, and assume an alias for the individual in your there-exists statement. Get to ∃((x: T) => P(x)) by the last line of the subproof. After the subproof, use ExistsE[T] to restate ∃((x: T) => P(x)).

   • Are you trying to prove something of the form p →: q?

     • Use ImplyI. Open a subproof, assume p, and get to q by the end of the subproof. After the subproof, use ImplyI to conclude p →: q.

   • Are you trying to prove something of the form ¬p?

     • Use NegI. Open a subproof, assume p, and get a contradiction, F, by the end of the subproof. After the subproof, use NegI to conclude ¬p.

   • Are you trying to prove something of the form p ∧ q?

     • Try to prove p by itself and then q by itself. Afterward, use AndI to conclude p ∧ q.

   • Are you trying to prove something of the form p ∨ q?

     • See if you have either p or q by itself – if you do, use either OrI1 or OrI2 to conclude p ∨ q.

3. You’ll need to nest the approaches from step 2. Once you are in a subproof, think about what you are trying to prove by the end of that subproof. Follow the strategy in step 2 to prove your current goal, nesting subproofs as needed. As you work, stop and scan the claims that you have available. See if you can extract anything from them as you did for the premises in step 1.

4. No match, or still stuck?

   • Do you have a there-exists statement available? Try using ExistsE[T] to reach your goal.
   • Do you have an OR statement available? Try using OR elimination to prove your goal conclusion.
   • Do your statements have NOT operators, but don’t fit the form for using ¬i? Try using PbC. If you are trying to prove something of the form p, open a subproof, assume ¬p, and try to reach a contradiction by the end of the subproof. Afterward, use PbC to conclude p.
   • As a last resort, try pasting in the proof for the law of the excluded middle (see section 4.5). Then use OR elimination on p ∨ ¬p.

Think of doing a proof as solving a maze, and of all our deduction rules as possible directions you can turn. If you have claims that match a deduction rule, then you can try applying the rule (i.e, “turning that direction”). As you work, you may apply more and more rules until the proof falls into place (you exit the maze)…or, you might get stuck. If this happens, it doesn’t mean that you have done anything wrong – it just means that you have reached a dead end and need to try something else. You backtrack, and try a different approach instead (try turning in a different direction).

Soundness and Completeness

Soundness and completeness definitions

We now revisit the notions of soundness and completeness. We recall from propositional logic that a proof system is sound if everything that is provable is actually true. A proof system is complete if everything that is true can be proved.

Interpretations

When we write statements in logic, we use predicates and function symbols (e.g., ∀ i (i * 2) > i). An interpretation gives the meaning of:

• The underlying domain – what set of elements it names

• Each function symbol – what answers it computes from its parameters from the domain

• Each predicate – which combinations of arguments from the domain lead to true answers and false answers

Interpretation example - integers

Here is an example. Say we have the function symbols: +, -, *, and /, and the predicate symbols: > and =. What do these names and symbols mean? We must interpret them.

The standard interpretation of arithmetic is that:

• int names the set of all integers

• +, -, *, and / name the integer addition, subtraction, multiplication, and division functions (that take two integers as “parameters” and “return” an integer result)

• = and > name integer equality comparison and integer less-than comparison predicates (that take two integers as “parameters” and “return” the boolean result of the comparison)

With this interpretation of arithmetic, we can interpret statements. For example,∀ i (i * 2) > i interprets to false, as when i is negative, then i * 2 < i. Similarly, ∃ j (j * j) = j interprets to true, as 1 * 1 = 1.

Now, given the function names +, -, *, /, and the predicates, =, >, we can choose to interpret them in another way. For example, we might interpret the underlying domain as just the nonnegative integers. We can interpret +, *, /, >, = as the usual operations on ints, but we must give a different meaning to -. We might define m - n == 0, whenever n > m.

Yet another interpretation is to say that the domain is just {0, 1}; the functions are the usual arithmetic operations on 0 and 1 under the modulus of 2. For example, we would define 1 + 1 == 0 because (1 + 1) mod 2 == 0. We would define 1 > 0 as true and any other evaluation of < as false.

These three examples show that the symbols in a logic can be interpreted in multiple different ways.

Interpretation example - predicates

Here is a second example. There are no functions, and the predicates are IsMortal(_), IsLeftHanded(_) and IsMarriedTo(,). An interpretation might make all (living) members of the human race as the domain; make IsMortal(h) defined as true for every human h; make IsLeftHanded(j) defined as true for exactly those humans, j, who are left handed; and set IsMarriedTo(x, y) as true for all pairs of humans (x, y) who have their marriage document in hand.

We can ask whether a proposition is true within ONE specific interpretation, and we can ask whether a proposition is true within ALL possible interpretations. This leads to the notions of soundness and completeness for predicate logic.

Valid sequents in predicate logic

A sequent, P_1, P_2, ..., P_n ⊢ Q is valid in an interpretation, I, provided that when all of P_1, P_2, …, P_n are true in interpretation I, then so is Q. The sequent is valid exactly when it is valid in ALL possible interpretations.

Soundness and completeness in predicate logic

We can then define soundness and completeness for predicate logic:

soundness: When we use the deduction rules to prove that P_1, P_2, ..., P_n ⊢ Q, then the sequent is valid (in all possible interpretations)

completeness: When P_1, P_2, ..., P_n ⊢ Q is valid (in all possible interpretations), then we can use the deduction rules to prove the sequent.

Note that, if P_1, P_2, ..., P_n ⊢ Q is valid in just ONE specific interpretation, then we are not guaranteed that our rules will prove it. This is a famous trouble spot: For centuries, mathematicians were searching for a set of deduction rules that could be used to build logic proofs of all the true propositions of arithmetic, that is, the language of int, +, -, *, /, >, and =. No appropriate rule set was devised.

In the early 20th century, Kurt Gödel showed that it is impossible to formulate a sound set of rules customized for arithmetic that will prove exactly the true facts of arithmetic. Gödel showed this by formulating true propositions in arithmetic notation that talked about the computational power of the proof rules themselves, making it impossible for the proof rules to reason completely about themselves. The form of proposition he coded in logic+arithmetic stated “I cannot be proved”. If this proposition is false, it means the proposition can be proved. But this would make the rule set unsound, because it proved a false claim. The only possibility is that the proposition is true (and it cannot be proved). Hence, the proof rules remain sound but are incomplete.

Gödel’s construction, called diagonalization, opened the door to the modern theory of computer science, called computability theory, where techniques from logic are used to analyze computer programs. You can study these topics more in CIS 570 and CIS 575.

Computability theory includes the notion of decidability – a problem that is decidable CAN be solved by a computer, and one that is undecidable cannot. A famous example of an undecidable problem is the Halting problem: given an arbitrary computer program and program input, can we write a checker program that will tell if the input program will necessarily terminate (halt) on its input? The answer is NO - the checker wouldn’t work on itself.