@MSGID:
<08c8b172-2cb7-4343-b907-52066a383045n@googlegroups.com> f67c5692
@REPLY: 1@solani.org> c6e1ff2f
@REPLYADDR Mild Shock <bursejan@gmail.com>
@REPLYTO 2:5075/128 Mild Shock
@CHRS: CP866 2
@RFC: 1 0
@RFC-References: 1@solani.org>
1@solani.org> <69fe5f82-f386-4784-99fa-7c998be49093n@googlegroups.com>
1@solani.org>
@RFC-Message-ID:
<08c8b172-2cb7-4343-b907-52066a383045n@googlegroups.com>
@TZUTC: -0700
@PID: G2/1.0
@TID: FIDOGATE-5.12-ge4e8b94
We recently introduce a Prolog logic framework based on 
extended Clauses that provide embedded implication. We 
could also demonstrate minimal and classical cartesian 
logic with it. As a GUI improvement, you have to put down 
your rose coloured glasses to see the proof terms.

When desired we can now let the logic framework 
show proof terms in color red besides the types in 
color blue. A classical proof is seen in that the Felleisen 
C operator appears. As an exercise we investigate a 
claim by Ingebrigt Johansson that falsum is dispensable.

See also:

Wadler Glasses for Mathematical Logic
https://twitter.com/dogelogch/status/1682756064020758530

Wadler Glasses for Mathematical Logic
https://www.facebook.com/groups/dogelog

Mild Shock schrieb am Donnerstag, 20. Juli 2023 um 10:48:34 UTC+2:
> Now that we have a logic framework for propositional 
> logics, we use it to explore genuine negation in 
> cartesian logic. So far we use ~A = A -> f as an 
> abbrevation, so ~A was replaced before starting 
> the proof search. Now we present a cartesian logic 
> that has genuinly formulas of the form ~A. 
> 
> We use a notation change idea burried in Johansson 
> Ingebrigts Minimal Logic Paper from 1937. Further 
> the logic framework was extended by a generic 
> usage analysis. Our ~(A=>B) = A/\\~B duality 
> investigation could be replicated with the 
> new genuine negation. 
> 
> See also: 
> 
> Genuine Negation in Cartesian Logic 
> https://twitter.com/dogelogch/status/1681701492435058695 
> 
> Genuine Negation in Cartesian Logic 
> https://www.facebook.com/groups/dogelog 
> 
> Mild Shock schrieb:
> > We are currently investigating cartesian logic. To 
> > reduce the complexity of our endeavour we explored 
> > embedded implication as a means to provide a logic 
> > framework. We can show natural deduction and gentzen 
> > style proof search, as well as fitch proof rendering. 
> > 
> > We use a proof renderer that is based the rule/2 clauses 
> > for natural deduction and not by the right/2 and left/4 
> > clauses for Gentzen style. Toying with our ~(A->B) = (A/\\~B) 
> > example, we find that Gentzen style, although still non- 
> > deterministic, is 25-times faster than natural deduction. 
> > 
> > See also: 
> > 
> > Embedded Implication as a Logic Framework 
> > https://twitter.com/dogelogch/status/1681326945701593088 
> > 
> > Embedded Implication as a Logic Framework 
> > https://www.facebook.com/groups/dogelog
--- G2/1.0
 * Origin: usenet.network (2:5075/128)
SEEN-BY: 5001/100 5005/49 5015/255 5019/40 5020/715
848 1042 4441 12000
SEEN-BY: 5030/49 1081 5058/104 5075/128
@PATH: 5075/128 5020/1042 4441