There is no inconsistency either in or about Core Logic.

[Tennant, Neil]

To Jo Vidal-Rosset:


Your formula (2) is a theorem of Core Logic, as shown by the proof you give for it. So, why do you later claim that formula (2) is unprovable in Core Logic (your emphasis)?

Let # be the absurdity symbol. Let |- be deducibility in Core Logic.

Call your formula (2) T, for short.

We have |-T, i.e. T is a core theorem.

What you have shown further is that T,A,~A|-B.

The 'target sequent' that would be produced by dogmatically insisting on your entitlement to a use of unrestricted Cut:

 :T     T,A,~A:B


===============

     A,~A:B


is A,~A:B. But Core Logic does not have unrestricted Cut! Indeed, it has no cut rule at all (in the system itself).

However, an epistemically gainful version of Cut is admissible, to wit:

if X|-P (say, by core proof Pi) and P,Y|-Q (say, by core proof Sigma), then for some subset X' of X and some subset Y' of Y, we have either X',Y'|-Q or X',Y'|-#.

You can determine which it is by means of the computable binary function [Pi,Sigma] defined in my writings in RSL and my book. Applied to your example, [Pi,Sigma] is the obvious one-step proof of the sequent ~A,A:#. There is no inconsistency within the system of Core Logic; and there is no meta-inconsistency in anything one can prove about Core Logic! Thus far, the only 'meta-inconsistency' about Core Logic is what you yourself have claimed! But you have not proved your claim. Nor could you; your claim is inconsistent with metatheorems about Core Logic that have already been proved.


Neil Tennant

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210116/9acc4439/attachment-0001.html>