Skip to main content
16 events
when toggle format what by license comment
Oct 22, 2011 at 16:59 comment added Countably Infinite @D.M.: Only saw your comment right now. The first part of you comment probably refers to something along Dialectica, where we can manage to sneek in logical operators via functions. Yep.
Jun 26, 2011 at 0:07 comment added Daniel Mehkeri @Jan: Ahh. The first thing I ever wrote on Wikipedia. :-) Another thing is that a "strong" negation tends to be definable in mathematical contexts, so minimal logic tends to collapse to intuitionistic. Sure, you can rig negation so that P and "not"-P don't imply every Q; but to try to contain the consequences of 0=1 is something else!
Jun 9, 2011 at 18:31 comment added Countably Infinite @Andres: The intersection between paraconsistent logic and intuitionist logic (= paracomplete logic) is minimal logic. Although I had some hope a couple of years ago that paraconsistent logic is more consistent than other logics, it is not so. Assertions of the kind of Currys paradox which have the shape of a comprehension axiom lead still to inconsistencies in such a logic, since the inconsistency already arises in minimal logic.
Jan 15, 2011 at 15:54 comment added Andrés E. Caicedo @David: The only theoretical framework I know of that would allow something like that is paraconsistency. As I wrote in the answer, I do not think it is currently equipped to handle something with the expressive power of ZF, but contacting the experts in the field may be the best way to make sure.
Jan 15, 2011 at 12:59 comment added David Harris Andres, I think what you are saying is that if ZFC is inconsistent, then the inconsistency could be isolated and eliminated without undue trauma. My question is, are there situations where we could leave the inconsistency in place and yet still be able to do useful work?
Jan 15, 2011 at 4:09 comment added Andrés E. Caicedo @Ricky: I am thinking of global-$\Sigma_2$, but I haven't thought about the difference. I think more subtle would be to study what would survive if $\Sigma_n$-induction makes PA inconsistent (because then even the $\Delta_0$ fragment of ZF would be problematic).
Jan 15, 2011 at 2:17 comment added user5810 If "replacement is restricted to $\Sigma_2$-formulas" then it's precise formulation would become important. For what you're talking about, would the relation have to be total and/or a partial function?
Jan 14, 2011 at 23:36 history edited Andrés E. Caicedo CC BY-SA 2.5
added 764 characters in body
Jan 14, 2011 at 23:31 comment added Andrés E. Caicedo @David: Oh, I was addressing infinite theories since I would expect a mixture of the two situations (a significant fragment is consistent, and yet the whole is not, but any inconsistency takes too long to prove) would be what happens in practice in the (granted, unlikely) event something like ZFC is inconsistent.
Jan 14, 2011 at 23:28 comment added Andrés E. Caicedo @David: You can think of the paper by Woodin I mentioned as suggesting a way in which the informal discussion above could be quantified: Say that PA is inconsistent, but any formal proof of an inconsistency takes a very large number of steps, way beyond the length of any proof considered so far. By playing with the expressive coding power of PA, it can be that in fact, any proof that "PA proves an inconsistency" requires also a huge number of steps (though perhaps shorter that a direct proof of an inconsistency). [Though, sure, there may be completely unexpected non-mathematical shortcuts.]
Jan 14, 2011 at 23:27 comment added David Harris Andres, it appears the phenomenon you are referring to is that "most of T is consistent." This is not equivalent to "the contradiction is long." A finitely axiomatizable theory could still have the property that the only contradictions are long. Being able to work with either of these properties would be interesting.
Jan 14, 2011 at 23:22 comment added Andrés E. Caicedo @David: So we do not look for one. Even if we actively looked for one, it is possible that any direct proof of an inconsistency is unfeasibly long by our standards. We then have a situation were we are not actively developing tools to foresee a contradiction, since we do not expect one, and a direct proof of one would take too long for us to discover. Sure, there is a chance that eventually we will develop intuitions that cannot be fully formalized that will lead us to suspect a contradiction is hiding somewhere, but even this may be a very long process. That's the situation I was suggesting.
Jan 14, 2011 at 23:18 comment added Andrés E. Caicedo @David: This helps us to develop more accurate intuition and to refine our mental pictures about the theory and its consequences but, again, our knowledge may be seriously flawed although it is better than before. Say that $T$ is inconsistent, but the fragment of $T$ that we have seriously studied so far is not. We develop good intuitions about this fragment, and erroneously believe these intuitions apply to the whole. Most of our efforts center on developing the consequences of the consistent fragment, because it is the one we manage best. We do not seriously expect an inconsistency. (Cont.)
Jan 14, 2011 at 23:14 comment added Andrés E. Caicedo @David: Say we are studying an infinite theory $T$. Of course, at any given time, we have only seriously considered a finite fragment of $T$ and, perhaps, some very general consequences of the whole theory. There is a good chance our intuitions about $T$ are plain wrong in several important respects, since they have been developed from a limited pool of results. This is actually a common phenomenon: Based on our knowledge up to a point, we believe of two options $A$ and $B$ that $A$ must hold. Then we prove that $B$ holds, and this forces us to reexamine our supposed understanding. (Cont.)
Jan 14, 2011 at 18:03 comment added David Harris I am confused by the claim that "a theory is inconsistent but any deduction takes so long we do not know." Does the length of the deduction make it difficult to know that a theory is inconsistent? Might there not be techniques which would show it inconsistent, short of explicitly constructing such inconsistency?
Jan 14, 2011 at 16:54 history answered Andrés E. Caicedo CC BY-SA 2.5