Minimal logic per Ingebrigt Johansson - setup iset.mm to ease?

[David A. Wheeler]

Minimal logic per Ingebrigt Johansson is a subset of intuitionist logic
that also rejects the principle of explosion (ex falso quodlibet).
https://en.wikipedia.org/wiki/Minimal_logic

Since it looks like we're building up an intuitionistic set of axioms and theorems,
would it be too difficult to create it so that it avoids using theorems that
don't apply in minimal logic?

It's not clear to me what axioms need to
change in iset.mm to implement minimal logic instead... I imagine
others know right away :-).

--- David A. Wheeler

[Benoit]

Hi David,

I'm actually working on a "piecemeal" axiomatization of propositional calculus, which has intuitionistic and minimal calculus as subsets. It is due to
T. Thacher Robinson, Independence of two nice sets of axioms for the propositional calculus, Journal of Symbolic Logic, 1968
I just sent you my work in a separate email.

It looks like very little modifications are needed to make iset.mm compatible with it: replace ax-in1 with the minimalistic contraposition
ax-contrap $a |- ( ( ph -> -. ps ) -> ( ps -> -. ph ) ) $.
and then minimal calculus is simply obtained from this axiom set by removing ax-in2.

Benoît

[David A. Wheeler]

On Sat, 24 Feb 2018 11:03:09 -0800 (PST), Benoit <benoit...@gmail.com> wrote:
> It looks like very little modifications are needed to make iset.mm
> compatible with it: replace ax-in1 with the minimalistic contraposition
> ax-contrap $a |- ( ( ph -> -. ps ) -> ( ps -> -. ph ) ) $.
> and then minimal calculus is simply obtained from this axiom set by
> removing ax-in2.

Cool, thanks for the info! At the very least, I think that ought to be documented
in iset.mm. That particular "minimalistic contraposition" is already in iset.mm
as "con2", so we could just add a reference from ax-in1 to ~ con2.

A deeper integration is obviously possible between intuitionist logic and
minimal logic. That is, we could start in iset.mm with the
minimalistic contraposition, and then add ax-in1 later (or some other axiom
that enabled full intuitionistic logic). If we did,
we would have to move Duns Scotus and related theorems later, since I believe a
key point of minimal logic is to make those kinds of deductions impossible.
I think moving Duns Scotus and friends down later wouldn't be a bad idea.

However, I don't know if people *want* to do that kind of integration.
If not, then documenting it now seems like a good idea.

--- David A. Wheeler

[Jim Kingdon]

Documenting it in iset.mm seems like a good first step. As for avoiding explosion in proofs or otherwise bringing minimal logic into iset.mm, I'm not so sure. We're still only partway through getting the file to distinguish between classical and intuitionistic logic, so I'm not sure whether adding more kinds of logic to the same file would work out nicely or not. Of course, people who want to experiment with different logics should do so (for me it would likely be dependent type theory), but there are a variety of ways to do that.

Sort of unrelatedly, is minimal logic used for much? Part of what gets me interested in intuitionistic logic is that it has formed the basis for a whole lot of activity, such as being the logic used in coq, being (sort of, although this is complicated) the way things work in the type theory of the HoTT Book, providing the basis for constructive set theory, etc. My favorite article (sort of an intro, sort of just a fun romp through some interesting theorems) is "Five stages of accepting constructive mathematics" by Bauer which is cited in the Intuitionistic Logic Explorer bibliography. Not that it is a side by side comparison of different logics, just that it shows some of the things people are doing with constructive mathematics.

[David A. Wheeler]

On Sat, 24 Feb 2018 18:59:41 -0800, Jim Kingdon <kin...@panix.com> wrote:
> Documenting it in iset.mm seems like a good first step. As for avoiding explosion in proofs or otherwise bringing minimal logic into iset.mm, I'm not so sure. We're still only partway through getting the file to distinguish between classical and intuitionistic logic, so I'm not sure whether adding more kinds of logic to the same file would work out nicely or not. Of course, people who want to experiment with different logics should do so (for me it would likely be dependent type theory), but there are a variety of ways to do that.

*If* it's relatively easy to add it in stages, I'd say "may as well do it".
By that I mean, if it's possible to split into 2-3 axioms, some introduced
earlier than others (as appears to be the case), may as well do it now.
Then it'd be easier to move theorems where they don't depend on the later parts
as we go along.

After all, both set.mm and iset.mm already add axioms/definitions in stages
(e.g., propositional before predicate, and in set.mm the axiom of choice
is defined *after* weaker versions like countable choice).

The Wikipedia article makes it *appear* that it's pretty easy to define
minimal logic, and then turn it into intuitionistic logic with 1 or 2 more axioms.
That looks a lot like "ZF" vs. "ZFC" in set.mm. But I'm no expert.

--- David A. Wheeler

[Norman Megill]

Eric Schechter's _Classical and Nonclassical Logics: An Introduction to the Mathematics of Propositions_ (2005) presents a "basic logic" on which various propositional calculus systems can be built with additional axioms having names like contraction, expansion, positive paradox, mingle, explosion, fusion, not-elimination, and relativity.  His basic logic is weaker than what Robinson calls "minimal logic".  He describes about a dozen weaker-than-classical systems of propositional calculus (including intuitionistic and relevant) built on his basic logic by adding different sets of axioms.  I think he chose some of his basic axioms from Robinson's paper (which he references).  The book is intended for teaching and is quite readable.

I wouldn't mind seeing either basic logic or minimal logic presented first in iset.mm, then additional axioms added to build up to intuitionistic logic, and at each stage proving what we can.  If we want to use a different set of axioms in this way, it needn't be a major disruption, since the first thing we would do (once all the new axioms are present) is to prove the current ones as theorems, so that nothing later has to be reproved.  Then over time, by whomever is interested, theorems provable from weaker systems can be moved earlier as they get proved, similar to the what Jim is doing to eliminate ax-3 where possible.  In particular, someone interested in another logic (such as relevant) could reuse the basic logic results as a starting point to save duplicated effort.

Norm

[Jim Kingdon]

This sounds like a good plan for how we could add weaker logics to iset.mm without disrupting things or needing to do everything at once.

[Benoit]

Hi all,

As I wrote above, I'm currently working on a metamath axiomatization of propositional calculus based on [Robinson68] (reference above in the thread).  Although this is still very much a work in progress, I have resolved posting it here since it is very relevant to the thread.  All comments are welcome.

Please don't be put off by the labelling, which is a different concern.  My advice is to type "MM> w t /t 220 /a" (to have all the theorems on a single page, and because the typesetting is optimized for "alt_html"), and then look first at the following:
- mmdefinitions.html, which shows that it does not require too much work to adapt iset.mm to this axiom system,
- the introductory comment in mmtheorems1.html, which explains the nice properties of this axiom system,
- the TOC, mmtheorems.html, which shows how the "piecemeal" nature of this axiom system translates to the structuring of the database.

I am not a logician, but I put some thought into it, and thoroughly searched the literature.  I think the properties of the Kanger-Robinson axiom system explained in the introductory comment of mmtheorems1.html (completeness and independence, separation property, piecemeal nature to make intuitionistic and minimal calculi appear as subsystems) make it worth considering.

As Norm wrote above, axioms from other systems can be reproved very early on (I think they are all among the theorems I have already proved in propcalc.mm) and then every later statement can remain unchanged: there simply may be individual efforts, over time, to reprove some of these theorems from weaker axiom systems.

Benoit

[Norman Megill]

Below I transcribed the axioms for basic logic in Schechter, plus the additional axioms needed for intuitionistic logic.  (I hope I didn't make any typos.)  Unlike Robinson's minimal logic, basic logic can be used as a basis for many other weaker-than-classical logics such as relevant logic.  It also provides a basis for logics that do not hold classically such as paraconsistent logic.

Schechter proves many theorems, most with detailed proofs, as the axioms are introduced.  He sometimes devotes entire chapters to individual axioms.

Basic implication

a. modus ponens {ph, ph -> ps} |- ps
b. identity     |- ph -> ph
c. permutation  |- (ph -> (ps -> ch)) -> (ps -> (ph -> ch))
d. ->-prefixing |- (ph -> ps) -> ((ch -> ph) -> (ch -> ps))

Basic logic = basic implication plus:

a. adjunction            {ph, ps} |- ph /\ ps
b. left /\-elimination   |- (ph /\ ps) -> ph
c. right /\-elimination  |- (ph /\ ps) -> ps
d. left \/-introduction  |- ph -> (ph \/ ps)
e. right \/-introduction |- ps -> (ph \/ ps)
f. /\-introduction  |- ((ph -> ps) /\ (ph -> ch)) -> (ph -> (ps /\ ch))
g. \/-elimination  |- ((ps -> ph) /\ (ch -> ph)) -> ((ps \/ ch) -> ph)
h. Distributive law  |- (ph /\ (ps \/ ch)) -> ((ph /\ ps) \/ ch)
i. First contrapositive law  |- (ph -> -. ps) -> (ps -> -. ph)

Intuitionistic logic = basic logic plus:

a. contraction        |- (ph -> (ph -> ps)) -> (ph -> ps)
b. positive paradox   |- (ph -> (ps -> ph))
c. implicative explosion  |- ph -> (-. ph -> ps)
d. strong adjunction |- ph -> (ps -> (ph /\ ps))

Note that by adding strong adjunction, the adjunction rule becomes redundant.  However, the adjunction rule is needed to have a complete basic logic for other purposes.

Norm

[David A. Wheeler]

Is there a way to turn basic logic into minimal logic? There are a number of papers that discuss Logics between minimal logic and intuitionistic logic.

--- David A.Wheeler

[Norman Megill]

On Sunday, February 25, 2018 at 10:17:47 AM UTC-5, Norman Megill wrote:
...

g. \/-elimination  |- ((ps -> ph) /\ (ch -> ph)) -> ((ps /\ ch) -> ph)

should be

g. \/-elimination  |- ((ps -> ph) /\ (ch -> ph)) -> ((ps \/ ch) -> ph)

I'll edit the original post as well.

Norm

[Norman Megill]

On Sunday, February 25, 2018 at 10:34:15 AM UTC-5, David A. Wheeler wrote:

Is there a way to turn basic logic into minimal logic? There are a number of papers that discuss Logics between minimal logic and intuitionistic logic.

--- David A.Wheeler

Although Schechter doesn't mention minimal logic, I think it can be achieved by adding contraction, positive paradox, and strong adjunction to basic logic.  Positive paradox and strong adjunction are axioms of minimal logic.  From basic logic + contraction, the self-distributive law (= Robinson's 2.2 = our ax-2) can be proved.  Intuitionistic logic would become minimal logic plus implicative explosion.  The revised table is:

Basic implication

a. modus ponens {ph, ph -> ps} |- ps
b. identity     |- ph -> ph
c. permutation  |- (ph -> (ps -> ch)) -> (ps -> (ph -> ch))
d. ->-prefixing |- (ph -> ps) -> ((ch -> ph) -> (ch -> ps))

Basic logic = basic implication plus:

a. adjunction            {ph, ps} |- ph /\ ps
b. left /\-elimination   |- (ph /\ ps) -> ph
c. right /\-elimination  |- (ph /\ ps) -> ps
d. left \/-introduction  |- ph -> (ph \/ ps)
e. right \/-introduction |- ps -> (ph \/ ps)
f. /\-introduction  |- ((ph -> ps) /\ (ph -> ch)) -> (ph -> (ps /\ ch))
g. \/-elimination  |- ((ps -> ph) /\ (ch -> ph)) -> ((ps \/ ch) -> ph)
h. Distributive law  |- (ph /\ (ps \/ ch)) -> ((ph /\ ps) \/ ch)
i. First contrapositive law  |- (ph -> -. ps) -> (ps -> -. ph)

Minimal logic = basic logic plus:

a. contraction        |- (ph -> (ph -> ps)) -> (ph -> ps)
b. positive paradox   |- (ph -> (ps -> ph))

c. strong adjunction |- ph -> (ps -> (ph /\ ps))

Intuitionistic logic = minimal logic plus

a. implicative explosion  |- ph -> (-. ph -> ps)


Norm

[Benoit]

The implicational fragments of several different logics have been intensively studied, in particular in connection with combinatory logic. I recall these combinators and mention several axiomatizations in the comments of propcalc.mm, where I cite a website by Dolph Ulrich, which is worth reading.

From Norm's post, it appears that Schechter's "basic implication" is BCI. The implicational fragment of relevance logic can be axiomtized by BCIW, and intuitionistic implicational calculus can be axiomatized by BCKW (as well as KS, the axiomatization used in set.mm and iset.mm and propcalc.mm). But for instance, BCK implies I, so the axiom system of Schechter is not independent (and this is only for the implicational fragment). Schechter probably didn't care about independence: there is a trade-off between tayloring axioms for particular types of logic, and having a global independent system. But for a metamath style database, independence would be more desirable, IMHO.

It seems unlikely that there is a satisfactory way to "turn basic logic into minimal logic", as David asks, at least with simple axioms (but I'm not positive, I'll have to think about it). For a related example which shows that things could go wrong: although BCKW is an independent axiomatization of intuitionistic implicational calculus, BCKW+Peirce is dependent.

Benoit

[Norman Megill]

On Sunday, February 25, 2018 at 11:31:22 AM UTC-5, Benoit wrote:

The implicational fragments of several different logics have been intensively studied, in particular in connection with combinatory logic. I recall these combinators and mention several axiomatizations in the comments of propcalc.mm, where I cite a website by Dolph Ulrich, which is worth reading.

From Norm's post, it appears that Schechter's "basic implication" is BCI. The implicational fragment of relevance logic can be axiomtized by BCIW, and intuitionistic implicational calculus can be axiomatized by BCKW (as well as KS, the axiomatization used in set.mm and iset.mm and propcalc.mm). But for instance, BCK implies I, so the axiom system of Schechter is not independent (and this is only for the implicational fragment). Schechter probably didn't care about independence: there is a trade-off between tayloring axioms for particular types of logic, and having a global independent system. But for a metamath style database, independence would be more desirable, IMHO.

Schecter does show dependencies (and gives independence proofs as well).  In particular, he shows how to derive I from more than one system, including BCK I think.  However, K (positive paradox) is a rather strong axiom that doesn't hold in relevant logic, and I was somewhat surprised it is included in minimal logic.  In my chart, I mentioned that adjunction becomes redundant only because Schechter said so immediately after strong adjunction was introduced.  He probably shows all redundancies somewhere in the book, but they can be somewhat buried, and I don't have time to go through the whole book right now.  I should have amended my chart to say, "Adjunction, identity, and possibly others become redundant when the axioms of minimal logic are added."

The problem is that in order to present a hierarchy of systems, it is difficult (maybe impossible, not sure) to present axioms of a weaker system that don't become redundant when axioms for a stronger system are added.  However, excluding I because K is eventually introduced in minimal logic, would make the weaker systems incomplete and therefore useless to someone needing them as a starting point for another system.

In set theory there are redundant axioms such as Pairing that can be derived from stronger ones like Replacement.  We like to avoid the full strength of Replacement where possible, and thus we state Pairing as a separate but redundant axiom.  There are various ways this can be handled in practice.  For example, we can add a "(New usage is discouraged)" tag on identity but add a note that it is OK to use it in proofs from basic logic (since it can't be derived there).

IIRC the fact that identity can't be derived from basic implication was an open problem for many years, and was finally solved by EP Martin who turned it into a PhD thesis in 1978.
 

It seems unlikely that there is a satisfactory way to "turn basic logic into minimal logic", as David asks, at least with simple axioms (but I'm not positive, I'll have to think about it).

I am pretty sure the axioms I added to basic logic result exactly in minimal logic.  Unless what you mean is that we must avoid redundant axioms.

Norm

 

[Norman Megill]

I wonder if a way to keep axioms independent is to add previous axioms as antecedents or hypotheses.  For example K could be replaced by (ph -> ph) -> ( ph -> (ps -> ph)) so that identity couldn't be derived from it.  Of course, that is rather ugly. :)

Norm

[Benoit]

> > It seems unlikely that there is a satisfactory way to "turn basic logic into minimal logic", as David asks, at least with simple axioms (but I'm not positive, I'll have to think about it).
> I am pretty sure the axioms I added to basic logic result exactly in minimal logic.  Unless what you mean is that we must avoid redundant axioms.

Yes, I meant: "keeping independence" since without this constraint, you can simply add the standard axioms for minimal logic and not worry about anything !

On Sunday, February 25, 2018 at 7:46:37 PM UTC+1, Norman Megill wrote:

I wonder if a way to keep axioms independent is to add previous axioms as antecedents or hypotheses.  For example K could be replaced by (ph -> ph) -> ( ph -> (ps -> ph)) so that identity couldn't be derived from it.  Of course, that is rather ugly. :)

Yes, it's a clever trick. And you're right: it does not yield the nicest axioms ! But at least it works. Actually, in this particular case, K': ( p -> p') -> ( q - (p->p')) is a special case of K that does the job: BCIK' is an independent axiomatization of BCK. It has three distinct variables whereas yours has only two, but it is organic (no strict subformula is a tautology) contrary to the ones obtained via your trick.

Benoît

[Norman Megill]

Jipsen is using the term "logic" to refer to a lattice, which is an algebraic object that has little to do with propositional calculus (although it may provide a model for a propositional calculus).

Similar confusion arises with "quantum logic".  Some authors use to mean an orthomodular poset with additional properties (that often does not correspond to a propositional calculus) and other authors use it to mean a propositional calculus whose models are orthomodular lattices.  In the former case, they usually refer to the structures as "quantum logics", and the plural provides a hint that they are talking about posets.

A quick Google search shows other authors use "basic logic" to mean (introductory) classical first-order logic, and others use it to mean standard logic gates.

I think we are safe using Schechter's definition provided we reference it.

Norm

On Sunday, March 11, 2018 at 4:54:22 PM UTC-4, Jan Burse wrote:

The name basic logic (in Schechter) is already taken, or is it the same?
http://www.math.chapman.edu/~jipsen/structures/doku.php/basic_logic_algebras

Am Sonntag, 25. Februar 2018 19:15:25 UTC+1 schrieb Jan Burse:

HM, HI and HC, but not so much HN, are all covered
in the book I already mentioned. Here is a link:

Basic Proof Theory, Troelstra & Schwichtenberg
https://www.amazon.de/Theory-Cambridge-Theoretical-Computer-Science/dp/0521779111

Am Sonntag, 25. Februar 2018 19:14:04 UTC+1 schrieb Jan Burse:

The feature could identify HM (minimal), HI (intuitionistic)
and HC (classical). I did experiment with a further logic,

HN (paraconsistent but not paracomplete, do not add
double negation elimination, only Clavius Law, but not

much is reported of applications of it). These logics are all
not relevance logics, have a simpler semantics,

on top of residuated lattices...

Am Sonntag, 25. Februar 2018 19:08:41 UTC+1 schrieb Jan Burse:

Minimal Logic Hilbert Style Implicational Fragment HM:

     A -> (B -> A)
     http://us.metamath.org/mpeuni/ax-1.html

     (A -> (B -> C)) -> ((A -> B) -> (A -> C))
     http://us.metamath.org/mpeuni/ax-2.html

See Basic Proof Theory, Troelstra & Schwichtenberg
Minimal logic HM is paraconsistent and paracomplete.

If meta math would tell, look this proof uses this fragment,
by inspecting what axioms are used, this could be a nice feature.

The above book also contains info what axioms consist
larger fragments, i.e. connectives and quatifiers, which are

still considered minimal logic.

[Norman Megill]

I was simply describing what was on the page you referenced.  He calls it "basic logic algebras".  I don't see a reference to a propositional calculus on that page.

But even if he calls a propositional calculus using it as a model by the name "basic logic", it is not important.  Many mathematical terms are used for different things by different authors.  As long as we accompany our use with a reference to the author, I don't see a problem.

Norm

On Sunday, March 11, 2018 at 6:12:03 PM UTC-4, Jan Burse wrote:

There is no such reference by Jipsen that equates logic with lattice.
Can you show me please? His catalogue is about structures.
And some of the have "lattice" in their name and some of them
have "logic" their. The names are from the originial sources that

Jipsen has given as a reference to each structure. You find
well known structures such as Heyting algebra (related to
intuitionistic logic) and Boolean algebra (related to classical
logic). Also on my side there was neither an implication that

jipsen equates logic with lattices. But it happens, for example
that a Boolean Algebra has the property that it is also bounded
distributive lattice. And it also happens that there exists already
a structure named basic logic algebra. And they are not from

Jipsen. The references I found:

Source:

Ordered Algebraic Structures: Proceedings of
the Gainesville Conference ... herausgegeben
von Jorge Martínez, 2013. Ha98, NPM99

Now I need only to figure out what Ha98 and NPM99 are.

[Norman Megill]

On Sunday, March 11, 2018 at 7:00:51 PM UTC-4, Jan Burse wrote:

Not he calls it "basic logic algebras", its just a structure catalogue entry.
A structure with this name. Unfortunately his entry is a little incomplete,
the reference section is not filled.

 

Here you see an example of an entry that is completely filled:
http://www.math.chapman.edu/~jipsen/structures/doku.php/mv-algebras

It has a references section at the end.  Where did Schechter get the
name from?

From Schechter's book, "The logics of greatest philosophical interest in this book are classical, constructive (intuitionist), relevant, and fuzzy (Zadeh and Lukasiewicz), shown in the upper half of the diagram below.  These logics have a substantial overlap, which I call basic logic; it appears at the bottom of the diagram."

After the term "basic logic" he references a footnote, which reads: "That's my own terminology; be cautioned that different mathematicians use the word "basic" in different ways."

What terminology would you have preferred that he use?

Norm
 

I don't how high or low are the chances that Schechters basic
logic is related to basic logic algebra.

I have no idea what if any propositional calculus basic logic algebra models.  More information is needed about the mapping of the model (e.g. what value of the model does


 

Actually when I visited the catalogue, maybe I could have had the
goal to more closely look at the structures there and maybe find
a structure that is related to Schechter.

But I was visiting the catalogue for other reasons, and just acciedentially
stepped of the name basic logic algebra. I only remember a poor guy
who like 20 years ago called his Prolog system ECliPSe.

But then came Java, with the Eclipse IDE, and its virtualy impossible
to find this poor guy via Google anymore. So from SEO (Search Engine
Optimization) aspect, having a unique name is very important,

you wrote yourself that "Basic Logic" is also used in the more neutral
sense, of "Introductory Logic", not refering to Schechter. So I myself
had no chance at all to find something about Schechter Basic Logic

somewhere else, since this is such a vague name. But I knew the
catalogue from elsewhere. And Bingo there was some Basic Logic.
But it seems its not the same...yes or no. Basic Logic Algebra needs

a fusion operator. Not sure whether Schechter has also a fusion aspect...