Prior's paradox and Plato's Sophist

We can show that for any propositional function $Q$ that there is a proposition $h$ such that

$$Qh\to h\mathrm{\&}\mathrm{\exists }p(Qp\mathrm{\&}\mathrm{\neg }p)$$

Having something which if asserted (when $Q$ is interpreted as assertion) is true is no big deal. For instance take the proposition $\mathrm{\exists }xQx$. The interesting twist is that we can also devise a proposition ($\mathrm{\exists }p(Qp\mathrm{\&}\mathrm{\neg }p)$ itself ) which if asserted not only is true but also implies that something else false is also asserted. This is related to the paradoxes of non-being and falsehood in the Sophist. 

In Bealer's logic consider also a relation $D(a,b)$ holding iff and only $a=[\varphi (x){]}_x$ for $x$ the only free variable in some $\varphi$ and $b=[\varphi ([\varphi (x){]}_x)]$. Then consider the sentence $G(x)$ given by $\mathrm{\forall }y.D(x,y)\to \mathrm{\neg }T(y)$ for some predicate such that $T([\varphi ])\to \varphi$. Then consider $G([\mathrm{\forall }y.D(x,y)\to \mathrm{\neg }T(y){]}_x)$ to derive an abstract version of Gödel's result. The relationship between first- and higher- order logic is still not entirely clear.  It seems more a question of convenience and level of abstraction relevant to a particular application.

The game Sokoban (which is NP and PSPACE hard) offers a very elegant computational illustration of the essence of mathematical proofs and axiomatic-deductive systems in general (though of course Sokoban  is decidable): the layout of the walls and initial position of the boxes are the hypotheses and the goal position of the boxes is the theorem to be proved. The possible movements of the figure and the boxes are the logical rules.  It would be nice if we could have an analogous illustration of the computational structure of debates or the Platonic and Aristotelian dialectic.

Philosophical and formal awareness of the concept of computability was one of the most outstanding advances in the history of western philosophy (Church, Turing).  We need to find a characterization of incomplete axiomatic-deductive systems - from a very abstract point of view.

It would be interesting to study C. S. Peirce's presentation of quantifier logic: that is, to devise an axiomatic-deductive system for first-order logic in which all formulas must appear in prenex form. Or investigate the deeper significance of Skolemization. 

It is fascinating how category theory, which on the surface level involves higher cardinalities and huge ontological redundancy(recall that there is a functor of Set into the effective topos), becomes united to finitary combinatorics and computer science.   The high cardinalities are perhaps reflections of our way of looking at things, at our own epistemic imperfection, incompleteness and ambiguity - they are convenient fictions from which we can derive real and optimal computational results as well as conceptual architecture. The true significance of the Löwenheim-Skolem theorem concerns the logical potential of countable infinity which is a direct heir to the traditional paradoxes of infinity.