Infeasible inconsistency

[Tennant, Neil]

I can't say that anyone knows of any such system (let's call it Delta), but I'd like to know what argument anyone might give against the conjecture that the possibility that Joe Shipman is raising here is actually realized (without our knowing it) by the following:

Delta:   ZFC
P      :   Your favorite large-cardinal assumption
Q      :   Con_ZFC

--NT
________________________________
From: FOM <fom-bounces at cs.nyu.edu> on behalf of Joe Shipman <joeshipman at aol.com>
Sent: Sunday, December 13, 2020 8:47 AM
To: Foundations of Mathematics <fom at cs.nyu.edu>
Subject: Infeasible inconsistency

Does anyone know an interesting example of a consistent formal system in which
1) There is a statement not-P with a proof of infeasible length
2) There are statements Q such that P—>Q has a feasible proof, Q does not have a feasible proof, and not-Q is not provable

In other words, adding P as an axiom is not known to introduce a feasible inconsistency, but does allow feasible proofs of things which were either independent or previously had only infeasible proofs.

— JS

Sent from my iPhone
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20201214/22635967/attachment-0001.html>