Re: Godel proved maths inconsistent not incompleteness theorem

On Mon, 5 May 2008 12:59:51 -0700 (PDT), Charlie-Boo
<shymathguy@xxxxxxxxx> wrote:

On May 4, 10:06 am, David C. Ullrich <dullr...@xxxxxxxxxxx> wrote:
On Sat, 3 May 2008 08:47:55 -0700 (PDT), Charlie-Boo





<shymath...@xxxxxxxxx> wrote:
On Apr 29, 10:33 am, Aatu Koskensilta <aatu.koskensi...@xxxxxxxxx>
wrote:
On 2008-04-28, in sci.logic, Chris Menzel wrote:
[...]

I personally am very fond of Haskell, as befits someone with a healthy
interest in type theory and proof theory, and will as an appetiser
provide the following snippet of Haskell code -- which I haven't
bothered to check

You "haven't bothered to check" it?  So if someone discovers it
doesn't work then you can say you're not a liar?  (Sorry for bring
hypothetical.)

Why not?  Is there significance - especially Mathematical significance
- to posting a bunch of lines without even trying them out?

You really can't figure this out? There was no mathematical
significance to the post. There was a discussion of the merits
of various programming languages re proof checkers - the
significance of the post is to show why Haskell would be
an excellent choice. And the post was very successful in
that regard.

See, it wasn't actually addressed to _you_ personally,
but to the rest of us in the discussion.

A proof verifier that hasn't been verified - isn't that a bit ironic?

Not half as ironic as you lecturing us about all this and then
posting that hilarious spec regarding how a proof chekcer
should work.

You are so trigger-happy you don't see the context of something and
misinterpret it. I didn't say this is how a proof-checker works in
general. I said that this is one way to write a proof checker using a
theorem generator,

Supposing so - the fact that your outline simply doesn't
work, for reasons I explained yesterday, still makes all
this very funny.

Of course you don't see it that way. But everyone
else does. And will, for the rest of history, as long as an
archive of sci.logic exists somewhere in the galaxy.

thus showing there is not a "huge difference".

Trivial point.

C-B

 data Wff = In Var Var
          | Equ Var Var
          | Neg Wff
          | And Wff Wff
          | Or Wff Wff
          | Implies Wff Wff
          | Equiv Wff Wff
          | Forall Var Wff
          | Exists Var Wff
          deriving (Show, Eq)

 newtype Var = Var String

 -- Using these types, the axiom of extensionality could be expressed
 -- as follows, using a few helper functions

 in x y = In (Var x) (Var y)
 equ x y = Equ (Var x) (Var y)

 axiomExtensionality = Forall (Var "z") (("z" `in` "x") `equiv`
                                         ("z"`in` "y"))
                       `equiv`
                       ("x" `equ` "y")

 -- We could provide fixity declarations for the type constructors of
 -- the Wff type, and use the characters deserved for operators,
 -- allowing us to write wffs in a natural syntax as Haskell
 -- expressions. That's left as an exercise for the reader.

 -- The following function checks whether a wff A follows by modus
 -- ponens from the wffs B and C, i.e. A `followsByMpFrom` (B, C)
 -- is true if B is of the form C --> A.
 followsByMpFrom a ((b `Implies` c), d) | c == a && d == b = True
                                        | otherwise        = False
 followsByMpFrom _ _                                       = False

 -- A few test cases
 test1 = ("x" `in` "y")
         `followsByMpFrom`
         ((("y" `in` "x") `Implies` ("x" `in` "y")),
          ("y" `in` "x")) -- Should evaluate to True

 test2 = ("y" `in` "x")
         `followsByMpFrom`
         ((("y" `in` "x") `Implies` ("x" `in` "y")),
          ("y" `in` "x")) -- Should evaluate to False

Extending all this into a full proof-checker is trivial. If we have in
mind something that is not only a proof of concept sort of thing, we
would probably introduce a monad which would handle stuff like
extending embedded class abstraction signs in formulas, allowing for
abbreviations and so on (we need a monad here because we must keep
track of what variables have already been used and so on, a task which
otherwise requires tedious plumbing in a pure language).

--
Aatu Koskensilta (aatu.koskensi...@xxxxxxxxx)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
 - Ludwig Wittgenstein, Tractatus Logico-Philosophicus- Hide quoted text -

- Show quoted text -

David C. Ullrich- Hide quoted text -

- Show quoted text -- Hide quoted text -

- Show quoted text -

David C. Ullrich
.

Relevant Pages

  • Qi and the type of EVAL
    ... This was originally posted to the functional programming news group. ... but I can't really grasp the difference between ocaml types, haskell ... Many years ago when I was new to ML, having moved from Lisp, I met Mike ... But eval is not part of Qi type theory; so you cannot use it in type ...
    (comp.lang.lisp)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... interest in type theory and proof theory, ... provide the following snippet of Haskell code -- which I haven't ...  -- the Wff type, and use the characters deserved for operators, ... abbreviations and so on (we need a monad here because we must keep ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... interest in type theory and proof theory, ... provide the following snippet of Haskell code -- which I haven't ...  -- the Wff type, and use the characters deserved for operators, ... abbreviations and so on (we need a monad here because we must keep ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... I personally am very fond of Haskell, as befits someone with a healthy ... interest in type theory and proof theory, ...  -- The following function checks whether a wff A follows by modus ... abbreviations and so on (we need a monad here because we must keep ...
    (sci.logic)
  • Re: powerset
    ... I've found an explanation for Haskell programmers at this page: ... function and a monad. ... axiom 3. ... The trick is that there are monads defined for lists in Haskell. ...
    (comp.lang.lisp)
Quantcast