Posted: Mar 12, 2012 9:28 pm
by mizvekov
VazScep wrote:You'll find it a real pain to do any proofs. The biggest headache is the fact that you can't write things like:

Code: Select all
1) P  (assumption)
2) P => Q  (assumption)
3) Q  (MP 1,2)
4) P => (P => Q) => Q (1-3)


There's just nothing in the formal system which allows you to make assumptions like this and then discharge them at the end of a proof. And yet being able to do this makes things so much easier.

So the first thing you encounter in the proof theory of this sort of formal system is the "Deduction Theorem", which shows that any proof with explicit assumptions can always be translated into a proof which doesn't make explicit assumptions. And after writing my utilities module, the first thing I did was define a new proof language which allows for explicit assumptions, and then I wrote a "Deduction Function", which mirrors the Deduction Theorem exactly except that it is recursive where the theorem is inductive. This function transforms a proof in the new proof language into a true theorem from the logical kernel.

I see, thanks for the explanation.
I have one question though, is it of any utility here to do something like this:
Code: Select all
inst (\v -> if v == "p" then (theoremTerm (inst (\v -> Var v) axiom3)) else Var "b") axiom1

Ie getting the term of a theorem (using theoremTerm) and then using that to instantiate another axiom?