math-logic

Repository contains homework tasks from math logic course. Link to the course.

Requirement: alex, happy

hw0. Expression parser

Parses proposition with the following grammar:

Expr ::= Disj | Disj '->' Expr
Disj ::= Conj | Disj '|' Conj
Conj ::= Term | Conj '&' Term
Term ::= '!' Term | '(' Expr ')' | Name
Name = [A-Z] [A-Z 0-9]*

Lexer is generated by alex and Parser is generated by happy

Example

input:

P->!QQ->!R10&S|!T&U&V

output:

(->,P,(->,(!QQ),(|,(&,(!R10),S),(&,(&,(!T),U),V))))

hw1. Proof Checker for proposition

Checks given proof of a proposition and annotates each line deducing necessary rules. Complexity: O(N)

Example

input:

A,B|-A&B
A
B
A->B->A&B
B->A&B
A&B

output:

(1) A (Prop. 1)
(2) B (Prop. 2)
(3) (A)->((B)->((A)&(B))) (Ax. 3)
(4) (B)->((A)&(B)) (M.P. 3, 1)
(5) ((A)&(B)) (M.P. 4, 2)

hw2. Deduction theorem

Implementation of proof deduction theorem: transform given proof of Γ,A⊢B to Γ⊢A->B

input:

A|-B->A
A->B->A
A
B->A

output:

|-(A)->(A)
(A)->((A)->(A))
((A)->((A)->(A)))->(((A)->(((A)->(A))->(A)))->((A)->(A)))
((A)->(((A)->(A))->(A)))->((A)->(A))
(A)->(((A)->(A))->(A))
(A)->(A)

hw3. Completeness theorem for propositional calculus

Implementation of completeness theorem for zeroth-order logic: checks a1,a2,..,an ⊨ phi and builds the proof of a1,..,an ⊢ phi.

input:

B,W|=A->B

output:

B,W|-A->B
B->A->B
B
A->B

input:

|=!A&!B

output:

Proposition is false for A=T,B=F

hw4. Check properties of lattices

Checks that reflexive transitive closure of given graph is lattice with necessary properties.

Checked lattice's properties:

• join-semilattice: each two elements has a least upper bound (i.e. +/v is completely defined)
• meet-semilattice: each two elements has a least lower bound (i.e. -/∧ is completely defined)
• distributivity
• implicativity
• Boolean algebra: forall A . A+!A=1

input:

5
2 3 4
5
5
5
5

output:

refutation of destributivity: 2*(3+4)

hw6. Convert Heyting algebra to Kripke model (in progress)

Gets intuitionistic proposition and Kripke model which refutes that. Returns Heyting model that refutes the proposition.