Partially verifiable logic Are there any known or established or researched logics (not restricted to sequent logic) where the proof object


*

*Is not necessarily verifiable in every case whether the proof object is valid

*If it is verifiable, then it can be verified in finite time


The intention is that this logic would be more general than those restricted to primitive recursive computing models; for example, the proof of Godel's incompleteness theorem might not apply as usually presented.
 A: From the comments it seems that you want proof objects that are finite, even if they are potentially unverifiable. In the generalized incompleteness theorem a general formal system is simply a proof verifier program $V$ that halts on every input and accepts (the code of) $(x,y)$ iff $x$ is a (valid) proof of $y$. Your proposal then naturally corresponds to the idea of relaxing the requirement on $V$ and allowing it to not halt on inputs that it does not accept. It turns out that your proposal will still fall to the generalized incompleteness theorems, and we will have incompleteness for "verifiable" instead of "provable". Namely, we have the following results for your system $S$ where we say that $S \vdash P$ iff there is a verifiable proof of $P$ over $S$:


*

*You will never be able to use such a system to construct a program that decides the truth value (according to the meta-system) of every arithmetical sentence (or equivalently every sentence about finite binary strings) correctly. This follows easily from the unsolvability of the halting problem.

*If $S$ interprets PA$^-$ (equivalently TC) via a computable translation $ι$ of arithmetical sentences into $S$, and if $S \nvdash ι(0=1)$, then there is some arithmetical sentence $P$ such that $S \nvdash ι(P)$ and $S \nvdash ι(\neg P)$. The proof is the same as for the generalized incompleteness theorem linked above, except that $G$ performs the executions of $V$ in parallel, and so it does not matter that $V$ does not halt when it is unable to verify a proof. Indeed the stipulation that $V$ does halt when the proof can be verified is the crucial reason the proof works. Compared to (1), this requires $S$ to interpret PA$^-$, but does not care whether $S$ proves (the translation of) false arithmetical sentences. In other words, having mere arithmetical consistency is enough to force $S$ to be arithmetically incomplete, even if $S$ is arithmetically unsound.

*As mentioned in this more recent post explaining the generalized incompleteness theorem, the computability-based proof relativizes easily. So even if the proof verifier uses an uncomputable oracle, as long as the system can reason about programs using that same oracle, it will suffer incompleteness.
By the way, see this post for further discussion of reasons for or against wanting a foundational system to interpret $PA^-$, and a self-verifying theory of arithmetic that escapes incompleteness.
Anyway your questions are very interesting! I enjoyed thinking about them!
