Talk:Minimal logic

Synonymous with Positive (Propositional) Logic?

It seems that minimal logic is synonymous to positive propositional logic.

http://home.utah.edu/~nahaj/logic/structures/systems/ppl.html

http://home.utah.edu/~nahaj/logic/structures/systems/johansson.html

Although I think positive propositional logic is a misnomer, since I don't see a relationship to positive polarity of a propositional variable. Rather the term positive seems to stem from the fact that the logic does not have negation rules. This view is confirmed by the following encyclopedia entry:

"Logic in which the only arguments considered acceptable are those not connected with refutations, that is, with proofs of the falseness of propositions. Since the expression “A is false” is merely a variant of the expression ”not-A,” positive logic rejects any methods of introducing negation that involve methods of indirect proof, including proof by contradiction. It also rejects explicit definitions of negation of the type ⌝ A = dfA ⊃ f, where ⌝ is the negation symbol, ⊃ indicates implication, and f is a propositional variable or some “admissible” absurd assertion. Thus, positive logic may be said to be a logic without negation." The Great Soviet Encyclopedia (1979)

http://encyclopedia2.thefreedictionary.com/Positive+Logic

Jan Burse (talk) 11:16, 19 December 2012 (UTC)

The two terms are not synonymous. Positive logic is the positive fragment (i.e., with connectives $\to ,\land ,\lor$) of intuitionistic logic. In contrast, minimal logic has the full language of intuitionistic logic ($\to ,\land ,\lor ,\bot$), even though it has no rules specifically mentioning $\bot$, hence $\bot$ essentially acts as a name for an arbitrary constant. Since $\bot$ and $\neg$ are interdefinable ($\bot$ is equivalent to $\neg A\land \neg \neg A$ for any formula A), it is also possible to formulate minimal logic in the language $\to ,\land ,\lor ,\neg$, and then the difference becomes more pronounced: minimal logic includes some nontrivial properties of $\neg$, such as $(A\to \neg B)\to (B\to \neg A)$.—Emil J. 14:03, 19 December 2012 (UTC)

I'm not sure I would call that a nontrivial property of $\lnot$; after all $A\to (B\to C)$ is logically equivalent to $B\to (A\to C)$ (and this is provable constructively), and both of those formulas are in the positive fragment. As you said, $\bot$ is just a propositional variable from the point of view of minimal logic, so anything that it can prove about $\bot$ it can also prove about an arbitrary variable. But the difference in language is certainly a distinction between minimal logic and its positive fragment. — Carl (CBM · talk) 14:38, 19 December 2012 (UTC)

Let me clarify what I meant by the remark. If you rewrite ¬ in terms of → and ⊥, then of course $(A\to \neg B)\to (B\to \neg A)$ is an instance of $(A\to (B\to C))\to (B\to (A\to C))$ (and that’s the reason it holds in minimal logic in the first place). However, if you treat ¬ as a primitive connective, then $(A\to \neg B)\to (B\to \neg A)$ does not follow from any such schema. In other words, minimal logic in the language $\to ,\land ,\lor ,\neg$ cannot be axiomatized just by the axioms and rules of positive logic extended to the new language, one needs extra axioms as well, and this illustrates the point that it is different from positive logic. (A terminological quibble: syntactically, $\bot$ is not a propositional variable, it is a propositional constant (= nullary connective). This makes a difference for the definition of a substitution, for instance.)—Emil J. 14:56, 19 December 2012 (UTC)

Now I think it would be correct to say that minimal logic, is positive logic with the following axiom:

4.11 (a -> b)&(a -> ~b) -> ~a

The above is redundant under the stipulation ~A = (A -> f) for a new nullary constant. But it seems to me that Johansson wants to point out that 4.11 is needed in the first place, to legitimate ~A = (A -> f) and f = (~B & ~~B). Oki Doki.

Jan Burse (talk) 22:41, 23 December 2012 (UTC)

Your statement about the additional axiom is correct, according to the Introduction of Subminimal negation by Colacito et al. 2601:547:901:3690:44C0:45E6:FE05:5C50 (talk) 05:53, 28 February 2020 (UTC)

How is this weaker?

The description is not precise, but it leaves me with the impression that minimal logic is equivalent to intuitionistic. More precisely, that minimal logic proves all of the theorems of intuitionistic logic that can be stated without the bottom element, and that adjoining a bottom element to minimal logic would yield intuitionistic logic.

The argument in the article that minimal logic is "strictly weaker" appears to be simple confusion, mistakenly identifying the named proposition of minimal logic with the bottom element of intuitionistic logic, simply because the same symbol is assigned to both.

I get the impression something more superficial was meant, but the translation/retelling tried to make it more significant than it really is. Or maybe the original actually said something significant (i.e. my initial paragraph above is wrong), but the meaningful content was lost in the translation/retelling.

Hurkyl (talk) 23:07, 28 January 2018 (UTC)

Above all, the terminology here is specific to proof theory, or at least certain parts of it. Minimal logic differs from intuitionistic logic in its inference rules - they have the same language. In particular, minimal logic has no (special) inference rule for ⊥, and so a model in minimal propositional logic treats ⊥ like any other propositional variable. This is mentioned on p. 13 of these lecture notes by Towsner, for example [1]. So minimal logic can't prove⊥→P any more than it can prove Q→P. Intuitionistic logic adds the axiom scheme ⊥→φ for every formula φ, and as a consequence ⊥ has to be interpreted as false in every model of intuitionistic propositional logic. Minimal logic is not entirely trivial, though, as it can prove things like $\lnot \lnot \phi \to \phi$ and like $(\phi \to \psi )\to (\phi \to \lnot \psi )\to \lnot \phi$. As the article here says, any formula using only $\land ,\lor ,\to$ is provable in minimal logic if and only if it is provable in intuitionistic logic. More details on minimal logic are in Troesltra and Schwichtenberg Basic Proof Theory, chapter 2. — Carl (CBM · talk) 01:20, 29 January 2018 (UTC)

Tutorial tone

I placed a {{Tone}} template on the article because of frequent reliance on "tutorial tone". Examples include "Here we only cover theorems not included in the positive calculus...", "one can see that", "one can prove", "as we have seen", "Note, however, that" and other uses of "we" and "one". There are also self-references to article presentation such as "double negation formulas (below)", "also already spelled out above", etc. _signed, Willondon (talk) 13:13, 16 August 2022 (UTC)

Worth checking to see if its plagiarism from sources that's causing the tutorial tone. I'll dig a little but this field of math isn't my specialty. GabberFlasted (talk) 13:37, 16 August 2022 (UTC)

Greetings. I found the article understating some of its positive implication calculus derived theorems and stated the stronger versions, possibly with unintended "we's" here and there. I removed some now. I may make an account and clean it up more! In spite of prose, one could also make a list akin to the ones in the interdefinability section in the intuitionistic logic article - in fact, technically some of those listings should really be here and not there. While handy, they are not really special to that logic. The current article contains one of those too. I guess where the information went is a theory popularity thing, the intermediate logic page is also pretty sparse. For resources that are also online relating to what I had just added, the interesting short theorems are e.g. part of the agda (programming language) libraries and some is also on nLab, next to any books of course. But the proofs are all lambda calculus one-liners using the Brouwer–Heyting–Kolmogorov interpretation. Btw. this article has a short type theory section (seems to be here since a while), but that in turn also only concern a tiny subset of the logic. Those Wikipedia articles should be stratified - it's currently not so clear what information is where. However from the History page it doesn't seem to me that there's someone taking up any effort. Make requests if you have any. Best 212.95.5.203 (talk) 15:32, 16 August 2022 (UTC)

A lot of fine work has been done already! Cheers. I intended to visit the article tomorrow, when I had time to give it a good look. I didn't want to be the one that says "this should be fixed... not it!" I will have another look later tomorrow. I don't mind being the one that waits in the restaurant washroom thinking "OK, they must have all settled the cheque by now." _signed, Willondon (talk) 01:25, 17 August 2022 (UTC)