StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
primarykey
Id
1586891
data
AcceptedAnswerId
0
AnswerCount
0
ClosedDate
CommentCount
2
CommunityOwnedDate
2009-10-19T13:09:58.353
CreationDate
2009-10-19T04:00:04.967
FavoriteCount
0
LastActivityDate
2009-10-20T09:07:59.493
LastEditDate
2009-10-20T09:07:59.493
LastEditorUserId
169273
OwnerUserId
169273
ParentId
1581256
PostTypeId
2
Score
21
ViewCount
0
LastEditorDisplayName
text
Body
If You like "programming" in <a href="http://en.wikipedia.org/wiki/Combinatory_logic" rel="noreferrer">combinatory logic</a>, then <ul> <li>You can automatically "translate" some logic problems into another field: proving equality of combinatory logic terms.</li> <li>With a good functional programming practice, You can solve that,</li> <li>and afterwards, You can translate the answer back to a Hilbert style proof of Your original logic problem.</li> </ul> The possibility of this translation in ensured by <a href="http://en.wikipedia.org/wiki/Curry-Howard_correspondence" rel="noreferrer">Curry-Howard correspondence</a>. Unfortunately, the situation is so simple only for a subset of (propositional) logic: restricted using conditionals. Negation is a complication, I know nothing about that. Thus I cannot answer this concrete question: ¬ (α ⊃ ¬β)   ⊢   α But in cases where negation is not part of the question, the mentioned automatic translation (and back-translation) can be a help, provided that You have already practice in functional programming or combinatory logic. <hr> Of course, there are other helps, too, where we can remain inside the realm of logic: <ul> <li>proving the problem in some more intuitive deductive system (e.g. <a href="http://en.wikipedia.org/wiki/Natural_deduction" rel="noreferrer">natural deduction</a>)</li> <li>and afterwards using <a href="http://en.wikipedia.org/wiki/Metatheorem" rel="noreferrer">metatheorem</a>s that provide a "compiler" possibility: translating the "high-level" proof of natural deduction to the "machine-code" of Hilbert-style deduction system. I mean, for example, the metalogical theorem called "<a href="http://en.wikipedia.org/wiki/Deduction_theorem" rel="noreferrer">deduction theorem</a>".</li> </ul> <hr> As for theorem provers, as far as I know, the capabilities of some of them are extended so that they can harness interactive human assistance. E.g. <a href="http://en.wikipedia.org/wiki/Coq" rel="noreferrer">Coq</a> is such. <hr> <hr> <h1>Appendix</h1> Let us see an example. How to prove α ⊃ α? <h1>Hilbert system</h1> <ul> <li>Verum ex quolibetα,β is assumed as an axiom scheme, stating that sentence α ⊃ β ⊃ α is expected to be deducible, instantiated for any subsentences α,β</li> <li>Chain ruleα,β,γ is assumed as an axiom scheme, stating that sentence (α ⊃ β ⊃ γ) ⊃ (α ⊃ β) ⊃ α ⊃ γ is expected to be deducible, instantiated for any subsentences α,β</li> <li>Modus ponens is assumed as a rule of inference: provided that α ⊃ β is deducible, and also α is deducible, then we expect to be justified to infer that also α ⊃ β is deducible.</li> </ul> Let us prove theorem: α ⊃ α is deducible for any α proposition. Let us introduce the following notations and abbreviations, developing a "proof calculus": <h2>Proof calculus</h2> <ul> <li>VEQα,β:   ⊢   α ⊃ β ⊃ α </li> <li>CRα,β,γ:   ⊢   (α ⊃ β ⊃ γ) ⊃ (α ⊃ β) ⊃ α⊃ γ</li> <li>MP: If   ⊢   α ⊃ β and   ⊢   α, then also   ⊢   β</li> </ul> A tree diagram notation: <h3>Axiom scheme — Verum ex quolibet:</h3>     ━━━━━━━━━━━━━━━━━ [VEQα,β]           ⊢   α ⊃ β ⊃ α <h3>Axiom scheme — chain rule:</h3>     ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ [CRα,β,γ]           ⊢   (α ⊃ β ⊃ γ) ⊃ (α ⊃ β) ⊃ α⊃ γ <h3>Rule of inference — modus ponens:</h3>      ⊢   α ⊃ β           ⊢   α     ━━━━━━━━━━━━━━━━━━━ [MP]                      ⊢   β <h2>Proof tree</h2> Let us see a tree diagram representation of the proof: ━━━━━━━━━━━━━━━━━━━━━━━━━━━━ [CRα, α⊃α, α]    ━━━━━━━━━━━━━━━ [VEQα, α⊃α] ⊢   [α⊃(α⊃α)⊃α]⊃(α⊃α⊃α)⊃α⊃α                         ⊢   α ⊃ (α ⊃ α) ⊃ α ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ [MP]      ━━━━━━━━━━━ [VEQα,α]                                           ⊢   (α ⊃ α ⊃ α) ⊃ α ⊃ α                                              ⊢   α ⊃ α ⊃ α                                           ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ [MP]                                                                                      ⊢   α ⊃ α <h2>Proof formulae</h2> Let us see an even conciser (algebraic? calculus?) representation of the proof: (CRα,α⊃α,α VEQα,α ⊃ α) VEQα,α:   ⊢   α⊃ α so, we can represent the proof tree by a single formula: <ul> <li>the forking of the tree (modus ponens) is rendered by simple concatenation (parentheses),</li> <li>and the leaves of the tree are rendered by the abbreviations of the corresponding axiom names.</li> </ul> It is worth of keep record about the concrete instantiation, that' is typeset here with subindexical parameters. As it will be seen from the series of examples below, we can develop a proof calculus, where axioms are notated as sort of base combinators, and modus ponens is notated as a mere application of its "premise" subproofs: <h3>Example 1</h3> VEQα,β:   ⊢   α ⊃ β ⊃ α meant as Verum ex quolibet axiom scheme instantiated with α,β provides a proof for the statement, that α ⊃ β ⊃ α is deducible. <h3>Example 2</h3> VEQα,α:   ⊢   α ⊃ α ⊃ α Verum ex quolibet axiom scheme instantiated with α,α provides a proof for the statement, that α ⊃ α ⊃ α is deducible. <h3>Example 3</h3> VEQα, α⊃α:   ⊢   α ⊃ (α ⊃ α) ⊃ α meant as Verum ex quolibet axiom scheme instantiated with α, α⊃α provides a proof for the statement, that α ⊃ (α ⊃ α) ⊃ α is deducible. <h3>Example 4</h3> CRα,β,γ:   ⊢   (α ⊃ β ⊃ γ) ⊃ (α ⊃ β) ⊃ α⊃ γ meant as Chain rule axiom scheme instantiated with α,β,γ provides a proof for the statement, that (α ⊃ β ⊃ γ) ⊃ (α ⊃ β) ⊃ α⊃ γ is deducible. <h3>Example 5</h3> CRα,α⊃α,α:   ⊢   [α ⊃ (α⊃α) ⊃ α] ⊃ (α ⊃ α⊃α) ⊃ α⊃ α meant as Chain rule axiom scheme instantiated with α,α⊃α,α provides a proof for the statement, that [α ⊃ (α⊃α) ⊃ α] ⊃ (α ⊃ α⊃α) ⊃ α⊃ α is deducible. <h3>Example 6</h3> CRα,α⊃α,α VEQα,α ⊃ α:   ⊢   (α ⊃ α⊃α) ⊃ α⊃ α meant as If we combine CRα,α⊃α,α and VEQα,α ⊃ α together via modus ponens, then we get a proof that proves the following statement: (α ⊃ α⊃α) ⊃ α⊃ α is deducible. <h3>Example 7</h3> (CRα,α⊃α,α VEQα,α ⊃ α) VEQα,α:   ⊢   α⊃ α If we combine the compund proof (CRα,α⊃α,α) together with VEQα,α ⊃ α (via modus ponens), then we get an even more compund proof. This proves the following statement: α⊃ α is deducible. <h1>Combinatory logic</h1> Although all this above has indeed provided a proof for the expected theorem, but it seems very unintuitive. It cannot be seen how people can "find out" the proof. Let us see another field, where similar problems are investigated. <h2>Untyped combinatory logic</h2> <a href="http://en.wikipedia.org/wiki/Combinatory_logic" rel="noreferrer">Combinatory logic</a> can be regarded also as an extremely minimalistic functional programming language. Despite of its minimalism, it entirely Turing complete, but evenmore, one can write quite intuitive and complex programs even in this seemingly obfuscated language, in a modular and reusable way, with some practice gained from "normal" functional programming and some algebraic insights, . <h2>Adding typing rules</h2> Combinatory logic also has typed variants. Syntax is augmented with types, and evenmore, in addition to reduction rules, also typing rules are added. For base combinators: <ul> <li>Kα,β is selected as a basic combinator, <a href="http://en.wikipedia.org/wiki/Type_inhabitation" rel="noreferrer">inhabiting type</a> α → β → α</li> <li>Sα,β,γ is selected as a basic combinator, inhabiting type (α → β → γ) → (α → β) → α → γ.</li> </ul> Typing rule of application: <ul> <li>If X inhabits type α → β and Y inhabits type α, then X Y inhabits type β.</li> </ul> <h3>Notations and abbreviations</h3> <ul> <li>Kα,β: α → β → α</li> <li>Sα,β,γ: (α → β → γ) → (α → β)* → α → γ.</li> <li>If X: α → β and Y: α, then X Y: β.</li> </ul> <h1>Curry-Howard correspondence</h1> It can be seen that the "patterns" are isomorphic in the proof calculus and in this typed combinatory logic. <ul> <li>The Verum ex quolibet axiom of the proof calculus corresponds to the K base combinator of combinatory logic</li> <li>The Chain rule axiom of the proof calculus corresponds to the S base combinator of combinatory logic</li> <li>The Modus ponens rule of inference in the proof calculus corresponds to the operation "application" in combinatory logic.</li> <li>The "conditional" connective ⊃ of logic corresponds to type constructor → of type theory (and typed combinatory logic)</li> </ul> <h1>Functional programming</h1> But what is the gain? Why should we translate problems to combinatory logic? I, personally, find it sometimes useful, because functional programming is a thing which has a large literature and is applied in practical problems. People can get used to it, when forced to use it in erveryday programming tasks ans pracice. And some tricks and hints of functional programming practice can be exploited very well in combinatory logic reductions. And if a "transferred" practice develops in combinatory logic, then it can be harnessed also in finding proofs in Hilbert system. <h1>External links</h1> <h2>Links how types in functional programming (lambda calculus, combinatory logic) can be translated into logical proofs and theorems:</h2> <ul> <li>Wadler, Philip (1989). <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.9875" rel="noreferrer">Theorems for free!</a>. </li> </ul> <h2>Links (or books) how to learn methods and practice to program directly in combinatory logic:</h2> <ul> <li>Madore, David (2003). <a href="http://www.madore.org/~david/programs/unlambda/" rel="noreferrer">The Unlambda Programming Language. Unlambda: Your Functional Programming Language Nightmares Come True</a>.</li> <li>Curry, Haskell B. & Feys, Robert & Craig, William (1958). Combinatory Logic. Vol. I. Amsterdam: North-Holland Publishing Company.</li> <li>Tromp, John (1999). Binary Lambda Calculus and Combinatory Logic. Downloadable in PDF and Postscript from the author's <a href="http://homepages.cwi.nl/~tromp/cl/cl.html" rel="noreferrer">John's Lambda Calculus and Combinatory Logic Playground</a>.</li> </ul>
Tags
Title
singulars
PostAcceptedAnswerId
1. This table or related slice is empty.
PostParentId
1. POHilbert System - Automate Proof
 singulars
 PostTypePostTypeId
 PTQuestion
PostTypePostTypeId
1. PTAnswer
UserLastEditorUserId
1. USphysis
UserOwnerUserId
1. USphysis
plurals
PostLinksPostIdRelatedPostId
1. This table or related slice is empty.
PostLinksRelatedPostIdPostId
1. This table or related slice is empty.
PostsAcceptedAnswerId
1. POHilbert System - Automate Proof
 singulars
 PostTypePostTypeId
 PTQuestion
PostsParentIdCreationDate
1. This table or related slice is empty.
VotesPostIdCreationDate
1. VO
 singulars
 PostPostId
 PO
 UserUserId
 This table or related slice is empty.
 VoteTypeVoteTypeId
 VTUpMod
2. VO
 singulars
 PostPostId
 PO
 UserUserId
 This table or related slice is empty.
 VoteTypeVoteTypeId
 VTUpMod
3. VO
 singulars
 PostPostId
 PO
 UserUserId
 This table or related slice is empty.
 VoteTypeVoteTypeId
 VTUpMod
CommentsPostId
1. COWow I don't even understand this one at all, but I'm upvoting this if only on how awesome and through this post is!
 singulars
 PostPostId
 PO
 UserUserId
 USPharaun
2. COWe should be able to answer questions using Latex
 singulars
 PostPostId
 PO
 UserUserId
 USLuciano

Querying!

Guidance

A row detail

Detail views are divided into sections. All the information in the data section comes from columns in the selected row. The other sections display data from other, related rows.

Related data can be related in a to-one or a to-many fashion. Captions of data related in a to-many fashion link to a list view showing a filtered view of the table.

Try moving around until you find a non-empty to-many entry and click on the label to get to one. You can move back to the root by clicking on the database name in the header.