Re: FOL, ZFC, NGB and Prolog

galathaea wrote:

> tom wrote:
> (I thought Goedel equated provability and truth).
>
> to which aatu koskensita responded:
> Quite the opposite, really, provided we're speaking about formal
> provability.
>
>
> that is not quite true
> goedel, like many mathematicians of the time, struggled with the
> definition of truth
> and at times he did study the "truth as proof" school
> but his conceptions of its meaning was not a necessary component to his
> major arguments in metamathematics

I knew! :-LALALALA

> however, the constructivists of the time equated truth and provability
> and this later was incorporated into the foundations of computation
> which express the incompleteness theorems much more directly

Please, is the constructivists view mainstream today?

> the key concept is inaccesibility
> (or the dual notion of platonic truth)

That will take me 10 years to ponder. :-)

> to tom:

Yes, that's me. :-)

> if you are truly

Yes. Truly. Nothing else matters. :-)

> interested in the connections between computation and
> proof theory
> start with the curry-howard isomorphism
> it is the centerpiece on which the connection is made formal

I understand.

Peter Suber, Formal Systems and Machines - An Isomorphism
http://www.earlham.edu/~peters/courses/logsys/machines.htm

I am now going to implement all types of formal systems in Prolog. The
current situation is completely isomorphic to that with the TM and
whether it can be built solely with NANDs. I knew the answer, I could
not accept it without being solicited by an authority I unconditionally
accept. It all has to do with my cultural background. I love my country
and respect my teachers, still, they are wrong. I know I am right about
TMs and intelligence, and, IF this is not too much to ask, I beg for
help with ZFC and pattern matching. Three letters. Please.

-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
galathaea: prankster, fablist magician, liar

Always with utmost respect,
Tom

.

Relevant Pages