Exam COPY Flashcards
t is free for x in φ
if no free x leaf in φ occurs in the scope of ∀y or ∃y for
any variable y occurring in t.
Draw parse tree of following formula and give which variabels are bound or free
∀x ((P (x) → Q(x)) ∧ S(x, y))
What is the meaning of following notation
φ[t/x]
replacing all free occurrences of x in φ
by t
2017 - 1b
Free and bound variable
∀x ((P (x) → Q(x)) ∧ S(x, y))
establishing the validity of the sequent
Premiss x + 1 = 1 + x
Premiss (x + 1 > 1) → (x + 1 > 0)
Conclusion (1 + x) > 1 → (1 + x) > 0
Premiss ∀x (P (x) → Q(x))
Premiss ∃x P (x)
Conc. ∃x Q(x)
Prove folowing sequent
Premiss ∀x (P (x) → Q(x))
Premiss ∀x P (x)
Conc. ∀x Q(x)
Prove following sequent
Premiss P (t)
Premiss ∀x (P (x) → ¬Q(x))
Conc. ¬Q(t)
Prove the following sequent
Premiss ∀x .(P (x ) →Q (x ))
Conc. ∀x .¬Q (x ) →∀x .¬P (x )
Show general proof for
- For all introduction
- For all elimination
Exercise 1.2.1 - c
Premiss (p ∧ q) ∧ r
Conc p ∧ (q ∧ r)
Exercise 1.2.1 - e
Premiss q → (p → r)
Premiss ¬r
Premiss q
Conc. ¬p
Exercise 1.2.1 - f
Conc (p ∧ q) → p
Exercise 1.2.1 - h
Premiss p
Conc. (p → q) → q
Exercise 1.2.1- i
Premiss (p → r) ∧ (q → r)
Conc p ∧ q → r
Exercise 1.2.1 - j
Premiss q → r
Conc (p → q) → (p → r)
Exercise 1.2.1 - l
Premiss p → q
Premiss r → s
Conc p ∨ r → q ∨ s
Exercise 1.2.1 - n
Premiss (p ∨ (q → p)) ∧ q
Conc p
Exercise 1.2.1 - o
Premiss p → q, r → s
Conc p ∧ r → q ∧ s
Exercise 1.2.1 - r
Premiss p → q ∧ r
Conc (p → q) ∧ (p → r)
Exercise 1.2.1 - v
Premiss p ∨ (p ∧ q)
Conc p
Exercise 1.2.1 - x
Premiss p → (q ∨ r)
Premiss q → s
Premiss r → s
Conc p → s
Exercise 1.2.1 - y
Premiss (p ∧ q) ∨ (p ∧ r)
Conc p ∧ (q ∨ r)
Exercise 1.2.2 - a
Premiss ¬p → ¬q
Conc q → p
Exercise 1.2.2 - b
Premiss ¬p ∨ ¬q
Conc ¬(p ∧ q)
Exercise 1.2.2 - c
Premiss ¬p
Premiss p ∨ q
Conc q
Exercise 1.2.2 - d
Premiss p ∨ q
Premiss ¬q ∨ r
Conc p ∨ r
Exercise 1.2.2 - e
Premiss p → (q ∨ r)
Premiss ¬q
Premiss ¬r
Conc ¬p
Exercise 1.2.2 - f
Premiss ¬p ∧ ¬q
Conc ¬(p ∨ q)
Exercise 1.2.2 - g
Premiss p ∧ ¬p
Conc ¬(r → q) ∧ (r → q)
Exercise 1.2.2 - i
Premiss ¬(¬p ∨ q)
Conc p
exercise 1.2.3 - d
Conc ¬p → (p → (p → q))
Exercise 1.2.3 - n
Premiss p ∧ q
Conc ¬(¬p ∨ ¬q)
Prop logic - Semantics Exercise 1.4.2 - c
Compute the complete truth table of the formula
p ∨ (¬(q ∧ (r → q)))
Prop logic - semantic 1.4.4 - b
Compute the truth value on the formula’s parse tree, or specify the corresponding
line of a truth table where
p evaluates to F, q to T and the formula is
p → (¬q ∨ (q → p))
Prop logic - semantic 1.4.4 - c
Compute the truth value on the formula’s parse tree, or specify the corresponding
line of a truth table where
the formula is
¬((¬q ∧ (p → r)) ∧ (r → q))
p evaluates to F, q to T and r evaluates to T
Prop logic - semantic - 1.4.5
A formula is valid if all its valuations evaluate to true. A formula is satisfiable if it evaluates to true for at least one of its valuations.
Is the following formula valid ? Is it satisfiable ?
Prop logic - semantic 1.4.12
Premiss p → (q → r)
Conc p → (r → q)
Show that the above sequent is not valid by finding a valuation in which the truth values of the premiss formulas are true but the formula for conclusion is false
prop logic - semantic 1.4.13 a
Premiss p ∨ q
Conc p ∧ q
give examples of natural language
declarative sentences for the atoms p and q such that the premises are true,
but the conclusion false
prop logic - semantic 1.4.13 b
Premiss ¬p → ¬q
Conc ¬q → ¬p
give examples of natural language
declarative sentences for the atoms p and q such that the premises are true,
but the conclusion false
Prop logic - deduction 1.2.3 q
Conc (p → q) ∨ (q → r)
Using LEM
Exercise 2.3.9 - a
Prove the validity of the following sequents in predicate logic, where F , G, P ,
and Q have arity 1, and S has arity 0 (a ‘propositional atom’)
∃x (S → Q(x)) |− S → ∃x Q(x)
Exercise 2.3.9 - d
Prove the validity of the following sequents in predicate logic, where F , G, P ,
and Q have arity 1, and S has arity 0 (a ‘propositional atom’)
∀x P (x) → S |− ∃x (P (x) → S)
Exercise 2.3.9 - k
Prove the validity of the following sequents in predicate logic, where F , G, P ,
and Q have arity 1, and S has arity 0 (a ‘propositional atom’)
∀x (P (x) ∧ Q(x)) |− ∀x P (x) ∧ ∀x Q(x).
Exercise 2.3.9 - l
Prove the validity of the following sequents in predicate logic, where F , G, P ,
and Q have arity 1, and S has arity 0 (a ‘propositional atom’)
Premiss ∀x P (x) ∨ ∀x Q(x)
Conc ∀x (P (x) ∨ Q(x)).
Exercise 2.3.9 - m
Prove the validity of the following sequents in predicate logic, where F , G, P ,
and Q have arity 1, and S has arity 0 (a ‘propositional atom’)
∃x (P (x) ∧ Q(x)) |− ∃x P (x) ∧ ∃x Q(x).
Exercise 2.3.9 - n
Prove the validity of the following sequents in predicate logic, where F , G, P ,
and Q have arity 1, and S has arity 0 (a ‘propositional atom’)
∃x F (x) ∨ ∃x G(x) |− ∃x (F (x) ∨ G(x))
Exercise 2.3.9 - p
Prove the validity of the following sequents in predicate logic, where F , G, P ,
and Q have arity 1, and S has arity 0 (a ‘propositional atom’)
¬∀x ¬P (x) |− ∃x P (x).
Exercise 2.3.9 - q
Prove the validity of the following sequents in predicate logic, where F , G, P ,
and Q have arity 1, and S has arity 0 (a ‘propositional atom’)
∀x ¬P (x) |− ¬∃x P (x)
Exercise 2.3.9 - r
Prove the validity of the following sequents in predicate logic, where F , G, P ,
and Q have arity 1, and S has arity 0 (a ‘propositional atom’)
¬∃x P (x) |− ∀x ¬P (x)
Give all temporal connectives and some examples of formulas
- neXt
- Future state
- all future states (Globally)
- Until
- Release
- Weak-until
2016 - 1a
Premiss p → q
Premiss q → r
Premiss p → s
Conc p → (r ∧ s)
2016 - 1c
Premiss p ∨ q
Conc ¬q → p
Show examples of LTL connectives
Weak until - requires that a remains true until b becomes true, but does not
require that b ever does becomes true (i.e. a remains true
forever). It follows the expansion law of until.
2016 - 4b
Let P , S and M be unary predicates and R a binary predicate. Decide for each of the sequents below whether they are valid or not, i.e., give a
proof in natural deduction or a counter-model.
Premiss ∀x¬R(x, x)
Conc ∀x ∀y (R(x, y) → ¬R(y, x))
2016 - 4c
Let P , S and M be unary predicates and R a binary predicate. Decide for each of the sequents below whether they are valid or not, i.e., give a
proof in natural deduction or a counter-model.
Premiss ∀x ∀y (R(x, y) → ¬R(y, x))
Conc ∀z ¬R(z, z)
2016 - 4d
Let P , S and M be unary predicates and R a binary predicate. Decide for each of the sequents below whether they are valid or not, i.e., give a
proof in natural deduction or a counter-model.
Conc ∀x∃y R(x, y) ∨ ∀x∃y ¬R(x, y)
2016- 5b
Let P, Q, and R be unary predicate symbols, and f a unary function
symbol. Give proofs in natural deduction of the following sequents
Premiss ∀x (f (f (x)) = x)
Conc ∀x∃y (x = f (y))
Describe in text how to convert a truth table to
- DNF
- CNF
- For DNF look at the rows where the expression becomes True, think of it as “the expression can be true at row x OR row 2 OR …..
- For DNF look at the rows where the expression becomes False, think of it as “the expression cannot be false at row x and row 2 and …
2016 - 4a
Let P , S and M be unary predicates and R a binary predicate. Decide for each of the sequents below whether they are valid or not, i.e., give a
proof in natural deduction or a counter-model.
Premiss ∃x (P (x) ∧ ¬M (x))
Premiss ∃y (M (y) ∧ ¬S(y))
Conc ∃z(P (z) ∧ ¬S(z))
