Groups | Search | Server Info | Login | Register
| Newsgroups | sci.logic |
|---|---|
| Date | 2023-04-10 09:48 -0700 |
| References | (30 earlier) <008dc7f4-62ba-402c-93bb-d63aec6af7den@googlegroups.com> <e3246f22-9507-4852-9419-63a382b86201n@googlegroups.com> <ab97a223-5761-4050-982d-9408509051a1n@googlegroups.com> <2f0672c9-2e96-4203-9f28-c3f9a4c778e5n@googlegroups.com> <eba49114-1db2-4659-9934-acdf09e98213n@googlegroups.com> |
| Message-ID | <3d4d108c-7186-49b7-80a4-e7d7cdfc2059n@googlegroups.com> (permalink) |
| Subject | Re: What is the simplest way to learn model theory? |
| From | Mostowski Collapse <bursejan@gmail.com> |
Documentation tells me there is a show proof command? Maybe this can enlighten the question what proof Coq produces. Lets try manually "apply" example again: Coq < Lemma ex: forall (P Q R: Prop), P -> Q -> (P -> Q -> R) -> R. [... all the manual steps ...] ex < Show Proof. (fun (P Q R : Prop) (H : P) (J : Q) (K : P -> Q -> R) => K H J) Thats very nice! Great! Now lets try an automatic proof in Coq. The "auto" command of Coq cannot prove it. But the "intuition" command of Coq can prove it: Coq < Lemma ex: forall (P Q R: Prop), P -> Q -> (P -> Q -> R) -> R. ex < intuition. ex < Show Proof. (fun (P Q R : Prop) (H : P) (H0 : Q) (H1 : P -> Q -> R) => let H2 : Q -> R := H1 H in let H3 : R := H2 H0 in H3) The automatic proof of Coq is horrible. Its not doing linear beta reduction! Here is a preview, I get automatically what is not yet what the manual proof obtained. I first get: ∏1: ∏2: ∏3:(C ∏4:(∏5:(∏6:(4 6) (5 2)) (3 1))) I have some code that applies linear beta reduction and other reductions. In particular it can eliminate the Reductio 'C'. And then the result is simply: ∏1: ∏2: ∏3:(3 1 2) And the proof rendering: 1 p Premise 2 q Premise 3 p ⊃ q ⊃ r Premise 4 q ⊃ r Detach 3,1 5 r Detach 4,2 6 (p ⊃ q ⊃ r) ⊃ r ▲ Conclusion 3,5 7 q ⊃ (p ⊃ q ⊃ r) ⊃ r ▲ Conclusion 2,6 8 p ⊃ q ⊃ (p ⊃ q ⊃ r) ⊃ r ▲ Conclusion 1,7 The above proof search is not yet released. I am just toying around with it, to see whether its worth a release. Also I am not yet sure how to deal with the first order variant. The above is only propositional. But the first order variant might have some traps? Not yet sure. Mostowski Collapse schrieb am Montag, 10. April 2023 um 17:48:28 UTC+2: > Interestingly Howards paper contains both natural deduction > and sequent system. You find sequent system on page 483, > there is also the Coq "apply" rule, 5.2, and he mentions > > that it is the Gentzen LJ resp LK rule, via 5.1. He explicitly > has the heading "5. Normalization of terms and cut elimination", > so he does the same as Gentzen does, only he has > > proof terms available in the form of lambda expressions: > > The Formula-As-Types Notion of Construction > W.A.Howard - Manuscript 1969 (Publish 1980) > https://www.cs.cmu.edu/~crary/819-f09/Howard80.pdf > > So what is a Coq proof then? > Natural deduction or sequent system? > Mostowski Collapse schrieb am Montag, 10. April 2023 um 17:32:31 UTC+2: > > So you don't know? Why would Curry Howard be the > > reference for Natural Deduction? Doesn't make any sense. > > The term natural deduction was for example used > > > > in Gentzen, the abrevations there are NJ and NK; > > > > - Gentzen, Gerhard (1934–1935). "Untersuchungen über > > das logische Schließen". Mathematische Zeitschrift. 39: 405–431. > > > > On the other hand the Curry-Howard Isomorphism is not > > that old. Its much younger. You find it on the Wikipedia > > page mentioned, namely: > > > > - In 1969 Howard observes that another, more "high-level" proof > > system, referred to as natural deduction, can be directly interpreted > > in its intuitionistic version as a typed variant of the model of > > computation known as lambda calculus. > > > > If you only look at combinators you don't get natural deduction. > > You only get a Hilbert Style system. > > Julio Di Egidio schrieb am Montag, 10. April 2023 um 01:41:06 UTC+2: > > > On Monday, 10 April 2023 at 01:23:36 UTC+2, Mostowski Collapse wrote: > > > > > > > What is natural deduction? Can you explain? > > > Not to those who can't even be bothered to do a > > > text search in a given article. That WP page on > > > Curry-Howard, while I cannot guarantee for the > > > correctness, does provide a fairly comprehensive > > > overall picture... Asshole. > > > > > > *Plonk* > > > > > > Julio
Back to sci.logic | Previous | Next — Previous in thread | Next in thread | Find similar
What is the simplest way to learn model theory? olcott <polcott2@gmail.com> - 2023-04-07 00:50 -0500
Re: What is the simplest way to learn model theory? Python <python@invalid.org> - 2023-04-07 10:40 +0200
Re: What is the simplest way to learn model theory? Ross Finlayson <ross.a.finlayson@gmail.com> - 2023-04-07 09:32 -0700
Re: What is the simplest way to learn model theory? Jeffrey Rubard <jeffreydanielrubard@gmail.com> - 2023-04-07 13:10 -0700
Re: What is the simplest way to learn model theory? Ben Bacarisse <ben.usenet@bsb.me.uk> - 2023-04-07 21:56 +0100
Re: What is the simplest way to learn model theory? Ross Finlayson <ross.a.finlayson@gmail.com> - 2023-04-07 18:06 -0700
Re: What is the simplest way to learn model theory? olcott <polcott2@gmail.com> - 2023-04-07 20:30 -0500
Re: What is the simplest way to learn model theory? Ross Finlayson <ross.a.finlayson@gmail.com> - 2023-04-08 11:20 -0700
Re: What is the simplest way to learn model theory? Ross Finlayson <ross.a.finlayson@gmail.com> - 2023-04-08 12:57 -0700
Re: What is the simplest way to learn model theory? Ross Finlayson <ross.a.finlayson@gmail.com> - 2023-04-08 13:03 -0700
Re: What is the simplest way to learn model theory? olcott <polcott2@gmail.com> - 2023-04-07 23:25 -0500
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-08 00:59 -0700
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-08 01:07 -0700
Re: What is the simplest way to learn model theory? Julio Di Egidio <julio@diegidio.name> - 2023-04-08 06:02 -0700
Re: What is the simplest way to learn model theory? Julio Di Egidio <julio@diegidio.name> - 2023-04-08 16:36 +0200
Re: What is the simplest way to learn model theory? Julio Di Egidio <julio@diegidio.name> - 2023-04-08 17:23 +0200
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-08 09:01 -0700
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-08 09:09 -0700
Re: What is the simplest way to learn model theory? Julio Di Egidio <julio@diegidio.name> - 2023-04-08 09:21 -0700
Re: What is the simplest way to learn model theory? Julio Di Egidio <julio@diegidio.name> - 2023-04-08 09:24 -0700
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-08 09:31 -0700
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-08 09:36 -0700
Re: What is the simplest way to learn model theory? Julio Di Egidio <julio@diegidio.name> - 2023-04-08 18:59 +0200
Re: What is the simplest way to learn model theory? Mostowski Collapse <janburse@fastmail.fm> - 2023-04-08 19:29 +0200
Re: What is the simplest way to learn model theory? Mostowski Collapse <janburse@fastmail.fm> - 2023-04-08 19:50 +0200
Re: What is the simplest way to learn model theory? Dan Christensen <Dan_Christensen@sympatico.ca> - 2023-04-08 12:13 -0700
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-09 02:42 -0700
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-09 02:44 -0700
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-09 03:47 -0700
Re: What is the simplest way to learn model theory? Ross Finlayson <ross.a.finlayson@gmail.com> - 2023-04-09 10:08 -0700
Re: What is the simplest way to learn model theory? Dan Christensen <Dan_Christensen@sympatico.ca> - 2023-04-10 08:19 -0700
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-10 08:27 -0700
Re: What is the simplest way to learn model theory? Dan Christensen <Dan_Christensen@sympatico.ca> - 2023-04-10 10:53 -0700
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-10 12:42 -0700
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-10 12:59 -0700
Re: What is the simplest way to learn model theory? Dan Christensen <Dan_Christensen@sympatico.ca> - 2023-04-10 21:48 -0700
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-10 23:44 -0700
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-11 01:18 -0700
Re: What is the simplest way to learn model theory? Dan Christensen <Dan_Christensen@sympatico.ca> - 2023-04-11 08:55 -0700
Re: What is the simplest way to learn model theory? Julio Di Egidio <julio@diegidio.name> - 2023-04-09 03:48 -0700
Re: What is the simplest way to learn model theory? Julio Di Egidio <julio@diegidio.name> - 2023-04-09 03:52 -0700
Re: What is the simplest way to learn model theory? Julio Di Egidio <julio@diegidio.name> - 2023-04-09 16:57 +0200
Re: What is the simplest way to learn model theory? Julio Di Egidio <julio@diegidio.name> - 2023-04-09 17:24 +0200
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-09 10:44 -0700
Re: What is the simplest way to learn model theory? Julio Di Egidio <julio@diegidio.name> - 2023-04-09 11:23 -0700
Re: What is the simplest way to learn model theory? Julio Di Egidio <julio@diegidio.name> - 2023-04-09 13:52 -0700
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-09 14:04 -0700
Re: What is the simplest way to learn model theory? Julio Di Egidio <julio@diegidio.name> - 2023-04-09 14:12 -0700
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-09 14:14 -0700
Re: What is the simplest way to learn model theory? Julio Di Egidio <julio@diegidio.name> - 2023-04-09 14:25 -0700
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-09 14:26 -0700
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-09 14:29 -0700
Re: What is the simplest way to learn model theory? Julio Di Egidio <julio@diegidio.name> - 2023-04-09 14:43 -0700
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-09 14:59 -0700
Re: What is the simplest way to learn model theory? Julio Di Egidio <julio@diegidio.name> - 2023-04-09 15:20 -0700
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-09 15:46 -0700
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-09 15:50 -0700
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-09 15:59 -0700
Re: What is the simplest way to learn model theory? Julio Di Egidio <julio@diegidio.name> - 2023-04-09 16:12 -0700
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-09 16:23 -0700
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-09 16:29 -0700
Re: What is the simplest way to learn model theory? Julio Di Egidio <julio@diegidio.name> - 2023-04-09 16:40 -0700
Re: What is the simplest way to learn model theory? Julio Di Egidio <julio@diegidio.name> - 2023-04-09 16:41 -0700
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-10 08:32 -0700
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-10 08:48 -0700
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-10 09:48 -0700
Re: What is the simplest way to learn model theory? Julio Di Egidio <julio@diegidio.name> - 2023-04-11 06:35 -0700
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-11 16:22 -0700
Re: What is the simplest way to learn model theory? Julio Di Egidio <julio@diegidio.name> - 2023-04-09 15:57 -0700
Re: What is the simplest way to learn model theory? Ross Finlayson <ross.a.finlayson@gmail.com> - 2023-04-09 14:41 -0700
Re: What is the simplest way to learn model theory? Ben Bacarisse <ben.usenet@bsb.me.uk> - 2023-04-09 23:12 +0100
Re: What is the simplest way to learn model theory? Julio Di Egidio <julio@diegidio.name> - 2023-04-08 06:09 -0700
Re: What is the simplest way to learn model theory? [function defined] olcott <polcott2@gmail.com> - 2023-04-08 11:47 -0500
Re: What is the simplest way to learn model theory? [Ben Bacarisse] olcott <polcott2@gmail.com> - 2023-04-11 16:16 -0500
Re: What is the simplest way to learn model theory? olcott <polcott2@gmail.com> - 2023-04-07 16:16 -0500
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-07 14:24 -0700
Re: What is the simplest way to learn model theory? Mostowski Collapse <bursejan@gmail.com> - 2023-04-07 14:27 -0700
Re: What is the simplest way to learn model theory? olcott <polcott2@gmail.com> - 2023-04-07 16:33 -0500
Re: What is the simplest way to learn model theory? Julio Di Egidio <julio@diegidio.name> - 2023-04-07 14:52 -0700
Re: What is the simplest way to learn model theory? olcott <polcott2@gmail.com> - 2023-04-07 16:55 -0500
Re: What is the simplest way to learn model theory? Julio Di Egidio <julio@diegidio.name> - 2023-04-07 15:03 -0700
Re: What is the simplest way to learn model theory? olcott <polcott2@gmail.com> - 2023-04-07 17:15 -0500
Re: What is the simplest way to learn model theory? Julio Di Egidio <julio@diegidio.name> - 2023-04-07 15:21 -0700
Re: What is the simplest way to learn model theory? olcott <polcott2@gmail.com> - 2023-04-07 17:29 -0500
csiph-web