Path: ...!news.mixmin.net!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: sci.logic
Subject: Counter Example by Troelstra & Schwichtenberg (Was: Still on negative
 translation for substructural logics)
Date: Wed, 4 Dec 2024 08:47:41 +0100
Message-ID: <vip1eu$pniu$1@solani.org>
References: <vihumn$2eqeg$3@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 4 Dec 2024 07:47:42 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="843358"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
 Firefox/91.0 SeaMonkey/2.53.19
Cancel-Lock: sha1:QRGOaRoWSmjXnGOuUNCOrCuL/WY=
In-Reply-To: <vihumn$2eqeg$3@dont-email.me>
X-User-ID: eJwNyMkBwCAMA7CVSLFzjJOGev8RqJ7idvMJOB0UVb100mPELryYf1szac2jD8f92UZiMdMyULGCwyK2cngBYOsU9w==
Bytes: 4338
Lines: 95

Now I tried an example by Troelstra & Schwichtenberg:

?- solve_case(TT, schwichtenberg, G), time(solve_t__sel(TT, G)).
% 449 inferences, 0.000 CPU in 0.000 seconds (0% CPU, Infinite Lips)
false.

?- solve_case(TT, schwichtenberg2, G), time(solve_t__sel(TT, G)).
% 10,629 inferences, 0.000 CPU in 0.002 seconds (0% CPU, Infinite Lips)
false.

The definitions are this here:

solve_case(pos, schwichtenberg, [((((p->q)->q)->p)->q),(q->p)]=>q).
solve_case(neg, schwichtenberg2, [((((p->q)->q)->p)->q),(q->p)]=>q).

At least the second case shouldn't give false, as is seen here:

https://web.stanford.edu/class/cs103/tools/truth-table-tool/
p	q	((((((p → q) → q) → p) → q) ∧ (q → p)) → q)
F	F	T
F	T	T
T	F	T
T	T	T

It is a classical tautology, and if your TNT translation
is supposed to give a means to embed classical propositional
logic, the result of the second query should be true.

The example is from here, page 81, 3.5.6 remarks:

Basic Proof Theory, Cambridge University Press
A. S. Troelstra &  H. Schwichtenberg - June 2012
https://www.cambridge.org/core/books/basic-proof-theory/928508F797214A017D245A1FB67CCCD9

Helmut Schwichtenberg is still alive:
https://en.wikipedia.org/wiki/Helmut_Schwichtenberg

Anne Troelstra died in 2019:
https://en.wikipedia.org/wiki/Anne_Sjerp_Troelstra

Julio Di Egidio schrieb:
> On 01/12/2024 15:32, Mild Shock wrote:
> 
>  > So although it was very temping to download
>  > you software, and then replace these line:
>  > <https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11>
>  > By these line:
>  > notation(gliv(X), (~(~X)))
>  > solve_t__sel(neg, C=>X) :-
>  >     solve(C=>gliv(X)).
> 
> Or just change the definition of `dnt`, or create another one.  The code 
> is functional and pretty flexible actually, `notation/5` is `multifile`.
> 
>  > I am afraid I have no time for that. You
>  > could do it by yourself. Or what
> 
> I have already done it, and I have already told you the results!  You 
> have no time for anything apparently, except for posting random shit and 
> fucking with thread titles: I have messages all over the place, and it's 
> just me, you, and Ross once a month...
> 
> ---
> 
> Here is an interesting new case, which I had thought should be 
> *unsolvable*:
> 
> ```
> ?- solve_w([]=>dnt((~(~p)->p)<->p\/(~p))), !.  % DNE<->LEM
> ```
> 
> Unsolvable not just because my logic is *affine*, but because the actual 
> statement, provable intuitionistically, is intrinsically higher-order:
> 
> ```
> Theorem DNE_is_LEM : (forall p, ~ ~ p -> p) <-> (forall p, p \/ ~ p).
> ```
> 
> while the statement I am proving above is this one, and it is not 
> intuitionistically provable (AFAICT):
> 
> ```
> Theorem DNE_is_LEM_not_quite : forall p, (~ ~ p -> p) <-> (p \/ ~ p)
> ```
> 
> Yet with my `dnt`, my solver proves even that one (but I still have to 
> inspect the proof tree, what I actually get).  Indeed, I am rather 
> worried that it just solves everything I throw at it, though not the 
> falsities... which is why I am also developing a meta-theory for it, in 
> Coq:
> 
> <https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11#file-gentzen-v> 
> 
> 
> -Julio