----------------------------- TASK 1 DESCRIPTION: ----------------------------- Below you see the definition
pred p1(x:ℕ[3], y:ℕ[3]) ⇔ x > 0 ∧ y+1 = x ;
of a predicate p1(x,y) by a formula F with two free variables x,y; these variables (and all variables bound in F) may be assigned values from the domain ℕ[3] = { 0,1,2,3 }. TASK 1.a: Give all satisfying assignments of p1(x,y) by a comma-separated list << x-value , y-value >> , ... of all pairs of values from ℕ[3] that when assigned to x,y make p1(x,y) true:
Check the correctness of your answer:
If your answer is not correct, see here the number of satisfying assignments:
If your answer is still not correct, see here the satisfying assignments:
TASK 1.b: The formula p1(x,y) is satisfiable. True? (enter "true" or "false")
TASK 1.c: The formula p1(x,y) is valid. True? (enter "true" or "false")
----------------------------- TASK 2 DESCRIPTION: ----------------------------- Below you see the definition
pred p2(x:ℕ[3]) ⇔ ∃y:ℕ[3]. y+1 = x ;
of a predicate p2(x) by a formula F with one free variable x; this variable (and all variables bound in F) may be assigned values from the domain ℕ[3] = { 0,1,2,3 }. TASK 2.a: Give all satisfying assignments of p2(x) by a comma-separated list x-value , ... of all values from ℕ[3] that when assigned to x make p2(x) true.
TASK 2.b: The formula p2(x) is satisfiable. True? (enter "true" or "false")
TASK 2.c: The formula p2(x) is valid. True? (enter "true" or "false")
----------------------------- TASK 3 DESCRIPTION: ----------------------------- Below you see the definition
pred p3() ⇔ ∃y:ℕ[3]. ∀x:ℕ[3]. x > 0 ⇒ ∃y:ℕ[3]. y+1 = x ;
of a predicate p3() by a closed formula F. Give the truth value of p3() (enter "true" or "false"):
----------------------------- TASK 4 DESCRIPTION: ----------------------------- In the following we consider formulas interpreted over the domain ℕ[2] = { 0,1,2 }. Below you see two definitions
pred a4(p:Formula1, q:Formula1) ⇔ (∃x:ℕ[2]. p[x]) ∧ (∃x:ℕ[2]. q[x]) ; pred b4(p:Formula1, q:Formula1) ⇔ ∃x:ℕ[2]. p[x] ∧ q[x] ;
with formulas in which predicates p[x] and q[x] occur; please note that applications of these predicates have to be written with square brackets [ ]. Task 4.a: F2 a logical consequence of F1. True? (enter "true" or "false")
TASK 4.b: [ Only if your answer to TASK 4.a is "false". ] Give examples of two predicates p[x] and q[x] for which a4 is true and b4 is false. These examples may be simply written in the form of a two sequences p: p[0], p[1], p[2] q: q[0], q[1], q[2] of truth values that list the value of p[x] and q[x] for each value of x.
----------------------------- TASK 5 DESCRIPTION: ----------------------------- In the following we consider formulas interpreted over the domain ℕ[2] = { 0,1,2 }. Below you see a definition
pred a5(p:Formula1, q:Formula2) ⇔ ¬ ∀x:ℕ[2]. p[x] ⇒ ∃y:ℕ[2]. q[x][y] ;
with a formula in which predicates p[x] and q[x][y] occur; please note that applications of these predicates have to be written with square brackets [ ] around every argument. Give a definition
pred b5(p:Formula1, q:Formula2) ⇔
;
with a formula that is logically equivalent to the one given above but in which the negation connective ¬ is only applied to atomic formulas (i.e., "push the negation as much inside as possible"). Note: the following will only check the equivalence of your formula to the given one, not whether your formula indeed satisfies the syntactic description given above.
