User talk:Lord Farin/Backup/Definition:Classical Propositional Calculus

I am crashing into the boundaries of the possibilities the current state of PW allows me to go, since the axioms for Definition:Natural Deduction take, in some sense, three paths at once, using the notations for proofs with:

• $\vdash$
• vertical lines with annotation (convenient on paper, not so with TeX)
• tableaus

However it feels like the distinction between axioms and rules of inference is blurred when writing things like $(p\vdash q), p\vdash q$ (modus ponens) which is actually a rule of inference, and not an axiom as such (though presented as were it one).

There are LaTeX packages out there which allow for writing proof trees, but I have never liked how hard it is to read them when you didn't write them. I will proceed by incorporating the tableau proof method. In due time I will add the formalised interpretation of the sequent calculus (the one using $\vdash$). Sorry for any incoherence, this monologue took one hour to develop. --Lord_Farin 09:48, 16 June 2012 (EDT)

It just occurred to me that we probably want to reserve $\vdash$ for 'there exists a proof'; I also recall that the sequent calculus uses $\to$ instead. --Lord_Farin 09:50, 16 June 2012 (EDT)

If there's stuff you're running into problems with, leave them (perhaps use the "Help" template) and move on. I find this helps when I just need a break from a concept, and then suddenly everything falls into place.

Alternative techniques for demonstrating a proof (Tableau, truth table, natural deduction) are going to be difficult to resolve in a satisfactory way. My gut feeling is: the formal language approach has been taken as far as it need to with PropCalc, as the relevant and important theorem have been proved. The many detailed results which have been proved by natural deduction and truth table are probably also okay as they are - their validity has been demonstrated by the fact that the formal language approach has justified the natural deduction approach.

The hard work comes with PredCalc because it all becomes an order of magnitude more complicated. --prime mover 09:57, 16 June 2012 (EDT)

Thanks for the advice. I will move on reformatting the pages that exist, then at an appropriate moment get back to creating new stuff. --Lord_Farin 10:29, 16 June 2012 (EDT)

't Appears I am done with the restructuring of the language part of PredCalc as well. Now it is time to either move on to model theory and clean up the entangled mess over there in appropriate new categories like 'Boolean Model Theory (Propositional Calculus)' or delve into the realms of proof theory. Not sure which I find more appealing, so please indicate which one you feel is most desperate for a restructuring. In either case, room has to be created for future multiple approaches, be it Kripke models or different variants of natural deduction. --Lord_Farin 13:55, 18 June 2012 (EDT)

Model Theory sounds like a good plan, if you're up for it. It's an area I would rather not touch ... I don't have a vision for how it could all hang together. --prime mover 15:53, 18 June 2012 (EDT)

Having trouble to think of appropriate names for categories. For example, the PropCalc model theory of boolean interpret. could be Category:Boolean Interpretations or Category:Models for PropCalc/Boolean Interpretations. I think I like the latter better, but it's also longer (certainly when fully writing Propositional Calculus for PropCalc). There will be bool. interpr. for PredCalc as well (which is what is under 'PredCalc' in Definition:Model (Logic) atm) so something to discriminate these is required. Ideas/pref's? --Lord_Farin 18:23, 18 June 2012 (EDT)

I don't think we should be scared of long category names. If it needs a long name to specify it properly, then so be it. I have no problem with using PropCalc as an abbreviation, though. So Category:Models for PropCalc/Boolean Interpretations looks okay to me if that's what the category is all about. --prime mover 01:15, 19 June 2012 (EDT)

As the stuff is littered over a lot of different categories, I will need more time to develop an overview of what already exists. Please be patient. --Lord_Farin 09:17, 19 June 2012 (EDT)

No worries, take your time. --prime mover 11:50, 19 June 2012 (EDT)

You probably have noticed me continuing to chip away from the mountain of work still waiting. I am now getting into the final stage, at least for PropCalc, which inevitably includes separating out the proof systems, accordingly recategorize the soundness and completeness proofs that are out there and generally improve coherence.

On a practical note, I want to introduce a category 'Proof Systems for PropCalc' structured similar to Category:Models for PropCalc, but also feel that the distinction between classical and intuitionist PropCalc should be sustained. It would, however, be rather dull to have both system referring back and forth. Maybe the categories Category:Classical Propositional Calculus and :Category:Intuitionist Propositional Calculus could be replaced with definition pages in due time (some general page 'Definition:Proof Systems for PropCalc' incorporating or referring to all covered approaches, same for the models part. Probably you think I'm silly asking for encouragement every time, but with such large tasks at hand, I want to make sure that there will not be a dispute. So, am I still following the right tracks with these new ideas? --Lord_Farin 21:16, 26 June 2012 (UTC)

No, you do good to ask ...

I was never sure how to handle the categories "Classical PC" and "Intuitionist PC" in that the interesting thing about the latter was the results *not* included. I wonder whether to reserve that category, therefore, for "(whatever result) not valid in IPC" or whatever, and in CPC put those results which specifically depend upon LEM.

As for parallel threads based on different schemas, see how I have made a start on the axiomatic definitions of the natural numbers, specifically Principle of Finite Induction for a good example, and see whether you like what's done there. I think that uses the technique you suggested above. --prime mover 21:32, 26 June 2012 (UTC)

The trick/fun is that LEM allows infinitely many genuinely different weaker alternatives, among which are $(a\implies b)\lor(b\implies a)$ and variants. I think I'll keep away from filling up the two mentioned categories for the moment and just focus on structuring the currently present models and proof systems, adding rigour in the process. I'll save it for tomorrow and later, sleep has priority. On a side note, I like the stuff you put up on the $\N$-axiomatics and undoubtedly the style used in these realms will bear similarities to it. --Lord_Farin 21:46, 26 June 2012 (UTC)