Exercise: First Order Syntax

EXECUTION OPTIONS:
-----------------------------

(set if you want to minimize output)

GENERAL:
-------------
The following definitions are used for the remainder of this exercise.

val N = 10;    // the maximum number in our domain
type D = ℕ[N]; // the domain of numbers 0..N

Note that in the following checks, the requested syntactic properties of the
formulas that you enter will NOT be checked (only their equivalence to the given
formulas will be checked).

TASK 1 DESCRIPTION: 
-----------------------------
Below you see a formula F without parentheses:

¬ p(x) ∧ q(x) ⇒ r(x)

Give below a formula G which is identical to F except that it has a separate
pair of parentheses ( ) around *every* logical connective and around *every*
quantifier:

  (¬...) (...∧...) (...∨...) (...⇒...) (...⇔...) (∀...) (∃...)

Thus the number of parenthesis pairs ( ) to be added equals the total number of
connectives and quantifiers in F.

// Add here 3 pairs of parentheses ( )

TASK 2 DESCRIPTION: 
-----------------------------
Below you see a formula F without parentheses:

  ∃y:D. x + 1 = y

Give a definition of a formula G as described in the TASK 1 DESCRIPTION. However
*also* add in formula G a pair of parentheses ( ) around every application of an
infix function/predicate symbol:

   (...+...) (...=...) ...

// add here 3 pairs of parentheses ( )

TASK 3 DESCRIPTION: 
-----------------------------
Below you see the definition of a predicate by a formula F. Remove from the
parameter list all those variables x:D,... that are *not* free in F.

// remove here as many variables as possible
pred varFormula3(

) ⇔ 

  x < z ⇒ ∃y:D. y > 0 ∧ x+y = z

; 

Your answer is correct, if removing any more variables (after pressing the
"Check" button) would give an error message.

TASK 4 DESCRIPTION: 
-----------------------------
Below you see the description of an informal statement.

    x is greater than 0 and there is no such number
    (i.e., no number greater than 0) that is smaller than x
    (this means that x is the smallest number greater than 0.)
    

Give a definition of a predicate

   pred formula4(x:D,y:D,z:D) ⇔ F ;

with a formula F that expresses this statement in the *most literal* way (i.e.,
it should be a straight-forward translation from natural language to logic
operators).

Furthermore remove from "formula4(x:D,y:D,z:D)" all those variables that do
*not* occur freely in F.

Your answer is *very likely* correct if your definition (after pressing the
"Check" button does not give an error message and not the message "theorem is
not true".

// give here your formula F.
pred formula4(

) ⇔ // remove variables

  // replace "⊤"
; 

// correspondingly remove variables from application of formula here