LemmoNaDe Proof Constructor

Dependencies:

Goal formula:

Premises		Conclusion
	⊢

Edit Line:		Dependencies:	Formula:	Lines:	Rule:

Check the whole proof before exporting:
	Plain	Pretty Print	LaTexify

Paste a previously exported proof (in plain notation) here and import it by clicking the button. NOTE: you can edit a proof here, but you need to be careful about formatting. E.g. make sure the proof begins with a "Problem: " line, that formulas contain outermost parentheses, and that there are at least two spaces separating each "column" of the proof, with no double spaces elsewhere.

[+] Syntax

NOTE: formulas with a binary connective as their main connective should be enclosed by parentheses, as in the sample wffs below, but the program will accept such formulas without parentheses as well. The program will accept any lowercase letter as an individual constant or variable, so one could e.g. have '(Ea)Fa' or '(Fx>Gy)', but in practice it's best to notationally distinguish them as per the guidelines below. Note also that 'v' is reserved for disjunction, so it can't be used as a variable. See here for some (importable) sample proofs.

Logical Symbols
Negation	~
Conjunction	&
Disjunction	v
Conditional	>
Biconditional	<>
Existential Quantifier	E
Universal Quantifier	A
Identity Relation	=
Absurdity	#

Non-Logical Symbols
Individual Constants	a,b,c,d,e,f
Individual Variables	u,w,x,y,z
Propositional Constants	A ... Z
Predicate Constants (any arity)	A ... Z

Sample Wffs
P
((GvH)>F)
(#>P)
Fa
(Fa & Rab)
(Ex)Rxb
(Ex)(Ay)(Rxy <> Ryx)
(Ax)((Fx & (Ey)Rxy) > (Ey)(Fy v Ryx))
((Ax)(Fx > (Ey)Rxy) > (Ey)Gy)

[+] Rules for Sentential Logic

NOTE: the order in which rule lines are cited is important for multi-line rules. For example, in an application of conditional elimination with citation "j,k →E", the line j must be the conditional, and the line k must be its antecedent, even if line k actually precedes line j in the proof. The only multi-line rules which are set up so that order doesn't matter are &I and Df.


(j)	p	Premise
	___or___
(j)	p	Assumption

Rule of &I
a1..an	(j)	p
	:
b1..bu	(k)	q
	:
a1..an,b1..bu	(m)	p&q	j,k &I

Rule of &E
a1..an	(j)	p&q
	:
a1..an	(k)	p (or q)	j &E

Rule of →I
j	(j)	p	Assumption
	:
a1,..,an	(k)	q
	:
{a1..an}/j	(m)	p→q	j,k →I

Rule of →E
a1..an	(j)	p→q
	:
b1..bu	(k)	p
	:
a1..an,b1..bu	(m)	q	j,k →E

Rule of ~I
j	(j)	p	Assumption
	:
a1..an	(k)	⊥
	:
{a1..an}/j	(m)	~p	j,k ~I

Rule of ~E
a1..an	(j)	~q
	:
b1..bu	(k)	q
	:
a1..an,b1..bu	(m)	⊥	j,k ~E

Rule of DN
a1..an	(j)	~~p
	:
a1..an	(k)	p	j DN

Rule of vI
a1..an	(j)	p
	:
a1..an	(k)	pvq	vI j
		___or___
a1..an	(k)	qvp	j vI

Rule of vE
a1..an	(g)	pvq
	:
h	(h)	p	Assumption
	:
b1..bu	(i)	r
	:
j	(j)	q	Assumption
	:
c1..cw	(k)	r
	:
X	(m)	r	g,h,i,j,k vE
Where X = {a1..an}U{b1..bu}/hU{c1..cw}/j

Rule of Df
a1..an	(j)	(p→q)&(q→p)
	:
a1..an	(k)	p↔q	j Df

		__or__

a1..an	(j)	p↔q
	:
a1..an	(k)	(p→q)&(q→p)	j Df

Rule of EFQ
a1..an	(j)	⊥
	:
a1..an	(k)	p	j EFQ

[+] Rules for Quantificational Logic

Rule of ∀I
a1..an	(j)	φt
	:
a1..an	(k)	(Av)φv	j ∀I
where t is not in any of the formulae on lines a1..an and φv is obtained from φt by replacing every occurrence of t in φt with v, a variable not already in φt.

Rule of ∀E
a1..an	(j)	(∀v)φv
	:
a1..an	(k)	φt	j ∀E
where φt is obtained from φv by replacing every occurrence of v in φv with t.

Rule of ∃I
a1..an	(j)	φt
	:
a1..an	(k)	(∀v)φv	j ∃I
where φv is obtained from φt by replacing at least one occurrence of t in φt with v, a variable not already in φt.

Rule of ∃E
a1..an	(i)	(∃v)φv
	:
j	(j)	φt	Assumption
	:
b1..bu	(k)	ψ
	:
X	(m)	ψ	i,j,k ∃E
Where X = {a1..an}U{b1..bn}/j and t is not in (i) (∃v)φv, (ii) ψ, or (iii) any of the formulae at lines b1..bu other than j

Rule of =I
	(j)	t=t	=I
where t is any individual constant

Rule of =E
a1..an	(j)	t1=t2
	:
b1..bu	(k)	φt1
	:
a1..an,b1..bu	(m)	φt2	j,k =E
where φt2 is obtained from φt1 by replacing at least one occurrence of t1 in φt1 with t2.