
Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?
Posted:
Oct 12, 2012 8:52 PM


On 13 Oct, 10:45, rich...@cogsci.ed.ac.uk (Richard Tobin) wrote: > In article <458567d7d2984c8faf7d36473f1ae...@n16g2000yqi.googlegroups.com>, > > <camgi...@hush.com> wrote: > >> THERE IS, however, an algorithm that CONFIRMS that a formula is > >> logically valid WHEN IT IS. > >so why can't you do brute force lexicographically on ALL formulas and > >output > > >VALID > >NOT VALID >
> > Because there isn't an algorithm that confirms that a formula is > invalid when it is. > >  Richard
[GG] THERE IS, however, an algorithm that CONFIRMS that a formula is logically valid WHEN IT IS.
Use this!
if (valid(formula)) write (formula + " is valid") else write (formula + " is not valid")
What are you saying, valid() doesn't halt when the formula is invalid?
Herc

