...
Clausal Language (ver. 5.81.21, by P.J. Voda, J. Komara, J. Kluka)
Module  Ex07a in logic: Peano arithmetic
Included module  Standard
Remark 

Literature.

  • [1] Ján Komara. Specification and Verification of Programs. Online.

  • [2] Ján Kľuka. Úvod do deklaratívneho programovania. Online.

  • [3] Ján Komara. Recursive Functions. Online.

Remark 

Chapter. Quantification Logic.

Remark 

Section. Quantification Tableaux.

Remark 

[CL] Remark. The module Mlogicq in the file mlogicq.cl contains the syntax of tableau rules for quantifier tableaux. 

###
Theory  Examples in logic: first-order logic
Predicate  R  / 2
Remark 

Exercise. Prove the following sentence:

∃ y ∀ x R ( x , y ) → ∀ x ∃ y R ( x , y ) 
##
Theorem  Exists_forall
∃ y ∀ x R ( x , y ) → ∀ x ∃ y R ( x , y )
Predicate  A
Predicate  B
Remark 

Exercise. Prove the following sentences:

∃ x (A ( x ) ∧B ( x ) ) → ∃ x A ( x ) ∧ ∃ x B ( x ) ∀ x A ( x ) ∨ ∀ x B ( x ) → ∀ x (A ( x ) ∨B ( x ) ) ¬ ∃ x A ( x ) ↔ ∀ x ¬A ( x ) 
##
Theorem  Exists_and
∃ x (A ( x ) ∧B ( x ) ) → ∃ x A ( x ) ∧ ∃ x B ( x ) 
##
Theorem  Forall_or
∀ x A ( x ) ∨ ∀ x B ( x ) → ∀ x (A ( x ) ∨B ( x ) ) 
##
Theorem  Not_exists
¬ ∃ x A ( x ) ↔ ∀ x ¬A ( x )
End of theory  Examples
Remark 

Section. Logical Consequence.

Remark 

[CL] Remark. In the following examples you can use derived quantifier tableau rules as described in the module Mlogicd (see the file mlogicd.cl). 

###
Theory  Predicate_is_reflexive in logic: first-order logic with automatic rules
Predicate  R  / 2
Remark 

Exercise. Suppose that the binary predicate R (x,y) is symmetric and transitive:

Axiom  Symmetry
∀ x ∀ y (R ( x , y ) →R ( y , x ) )
Axiom  Transitivity
∀ x ∀ y ∀ z (R ( x , y ) ∧R ( y , z ) →R ( x , z ) )
Remark 

Show that the predicate is reflexive on its domain of definition: 

##
Theorem  Reflexivity
∀ x ( ∃ y R ( x , y ) →R ( x , x ) )
End of theory  Predicate_is_reflexive 
###
Theory  Predicate_is_asymmetric in logic: first-order logic with automatic rules
Predicate  R  / 2
Remark 

Exercise. Suppose that the binary predicate R (x,y) is ireflexive and transitive:

Axiom  Ireflexivity
∀ x ¬R ( x , x )
Axiom  Transitivity
∀ x ∀ y ∀ z (R ( x , y ) ∧R ( y , z ) →R ( x , z ) )
Remark 

Show that the predicate is asymmetric: 

##
Theorem  Asymmetry
∀ x ∀ y (R ( x , y ) → ¬R ( y , x ) )
End of theory  Predicate_is_asymmetric 
###
Theory  Predicate_is_identity in logic: first-order logic with automatic rules
Predicate  R  / 2
Remark 

Exercise. Suppose that the binary predicate R (x,y) is symmetric and antisymmetric:

Axiom  Symmetry
∀ x ∀ y (R ( x , y ) →R ( y , x ) )
Axiom  Antisymmetry
∀ x ∀ y (R ( x , y ) ∧R ( y , x ) → x = y )
Remark 

Show that the predicate is the identity on its domain of definition: 

##
Theorem  Identity
∀ x ∀ y (R ( x , y ) → x = y )
End of theory  Predicate_is_identity 
###
Theory  Equivalence_alternative_definition_of1 in logic: ☆Peano arithmetic
Predicate  R  / 2
Remark 

Exercise. (1 point) Suppose that the binary predicate R (x,y) is equivalence:

Axiom  Reflexivity
∀ x R ( x , x )
Axiom  Symmetry
∀ x ∀ y (R ( x , y ) →R ( y , x ) )
Axiom  Transitivity
∀ x ∀ y ∀ z (R ( x , y ) ∧R ( y , z ) →R ( x , z ) )
Remark 

Show that the predicate satisfies the property: 

##
Theorem  Alternative_definition
∀ x ∀ y (R ( x , y ) ↔ ∀ z (R ( x , z ) ↔R ( y , z ) ) )
End of theory  Equivalence_alternative_definition_of1 
###
Theory  Equivalence_alternative_definition_of2 in logic: ☆Peano arithmetic
Predicate  R  / 2
Remark 

Exercise. (1 point) Suppose that the binary predicate R (x,y) satisfies the property:

Axiom  Alternative_definition
∀ x ∀ y (R ( x , y ) ↔ ∀ z (R ( x , z ) ↔R ( y , z ) ) )
Remark 

Show that the predicate is equivalence: 

##
Theorem  Reflexivity
∀ x R ( x , x ) 
##
Theorem  Symmetry
∀ x ∀ y (R ( x , y ) →R ( y , x ) ) 
##
Theorem  Transitivity
∀ x ∀ y ∀ z (R ( x , y ) ∧R ( y , z ) →R ( x , z ) )
End of theory  Equivalence_alternative_definition_of2
Query:

Results:
Heap used: 251676 free: 133964024
Time used: 0:0:0:36