Oh, I see. So we can conclude, when we replace K by 15, that “If 1=0 is provable in PPT.2, then 1=0.” However, since we’re not actually working in PPT.2 anymore—we’ve replaced K by 15, which gave us a different proof system—then we don’t get an inconsistency.
Oh, I see. So we can conclude, when we replace K by 15, that “If 1=0 is provable in PPT.2, then 1=0.” However, since we’re not actually working in PPT.2 anymore—we’ve replaced K by 15, which gave us a different proof system—then we don’t get an inconsistency.
Exactly!