MOPA

In bounded arithmetic, we study weak fragments of arithmetic that often correspond in a certain sense to computational complexity classes (e.g., polynomial time). Questions about provability in such theories can be thought of as a form of feasible reasoning: considering a natural object of interest from a complexity class $C$, can we prove its fundamental properties using only concepts from $C$?

Our objects of interest in this talk will be the elementary integer arithmetic operations $+,-,\times,/$, whose complexity class is (uniform) $\mathrm{TC}^0$, a small subclass of $\mathrm{P}$. The corresponding arithmetical theory is $\mathit{VTC}^0$. Since we do not know yet if the theory can prove the totality of division and iterated multiplication $\prod_{i<n}X_i$ which are in $\mathrm{TC}^0$ by an intricate result of Hesse, Allender, and Barrington, we will also consider an extension of the theory $\mathit{VTC}^0+\mathit{IMUL}$.

Our main question is what can $\mathit{VTC}^0\pm\mathit{IMUL}$ prove about the elementary arithmetic operations. The answer is that more than one might expect: $\mathit{VTC}^0+\mathit{IMUL}$ proves induction for quantifier-free formulas in the basic language of arithmetic ($\mathit{IOpen}$), and even induction and minimization for $\Sigma^b_0$ (sharply bounded) formulas in Buss’s language. This result is connected to the existence of $\mathrm{TC}^0$ constant-degree root-finding algorithms; the proof relies on a formalization of a form of the Lagrange inversion formula in $\mathit{VTC}^0+\mathit{IMUL}$, and on model-theoretic abstract nonsense involving valued fields.

The remaining problem is if $\mathit{VTC}^0$ proves $\mathit{IMUL}$. We will discuss issues with formalization of the Hesse–Allender–Barrington construction in $\mathit{VTC}^0$, and some partial results (this is a work in progress).

Video

​

The usual base theory used in reverse mathematics, $\mathrm{RCA}_0$, is the fragment of second-order arithmetic axiomatized by $\Delta^0_1$ comprehension and $\Sigma^0_1$ induction. The weaker base theory $\mathrm{RCA}^*_0$ is obtained by replacing $\Sigma^0_1$ induction with $\Delta^0_1$ induction (and adding the well-known axiom $\exp$ in order to ensure totality of the exponential function). In first-order terms, $\mathrm{RCA}_0$ is conservative over $\mathrm{I}\Sigma_1$ and $\mathrm{RCA}^*_0$ is conservative over $\mathrm{B}\Sigma_1 + \exp$.

Some of the most interesting open problems in reverse mathematics concern the first-order strength of statements from Ramsey Theory, in particular Ramsey's Theorem for pairs and two colours. In this talk, I will discuss joint work with Kasia Kowalik, Tin Lok Wong, and Keita Yokoyama concerning the strength of Ramsey's Theorem over $\mathrm{RCA}^*_0$.

Given standard natural numbers $n,k \ge 2$, let $\mathrm{RT}^n_k$ stand for Ramsey's Theorem for $k$-colourings of $n$-tuples. We first show that assuming the failure of $\Sigma^0_1$ induction, $\mathrm{RT}^n_k$ is equivalent to its own relativization to an arbitrary $\Sigma^0_1$-definable cut. Using this, we give a complete axiomatization of the first-order consequences of $\mathrm{RCA}^*_0 + \mathrm{RT}^n_k$ for $n \ge 3$ (this turns out to be a rather peculiar fragment of PA) and obtain some nontrivial information about the first-order consequences of $\mathrm{RT}^2_k$. Time permitting, we will also discuss the question whether our results have any relevance for the well-known open problem of characterizing the first-order consequences of $\mathrm{RT}^2_2$ over the traditional base theory $\mathrm{RCA}_0$.

Video

​

In a paper with Kossak in 2018, we studied the notion of neutrality: a subset X of a model M of PA is called neutral if the definable closure relation in (M, X) coincides with that in M. This notion was suggested by Dolich. motivated by work by Chatzidakis-Pillay on generic expansions of theories. In this talk, we will look at a more direct translation of the Chatzidakis-Pillay notion of genericity, which we call 'CP-genericity', and discuss its relation to neutrality. The main result shows that for recursively saturated models, CP-generics are always neutral; previously we had known that not all neutral sets are CP-generic.

Video

​

Recall that if $M \subseteq N$ are models of set theory then $N$ end-extends $M$ if $N$ does not have new elements for sets in $M$. In this talk I will discuss a $\Sigma_1$-definable finite sequence which is universal for end extensions in the following sense. Consider a computably axiomatizable extension $\overline{\mathsf{ZF}}$ of $\mathsf{ZF}$. There is a $\Sigma_1$-definable finite sequence $$a_0, a_1, \ldots, a_n$$ with the following properties.

* $\mathsf{ZF}$ proves that the sequence is finite.
* In any transitive model of $\overline{\mathsf{ZF}}$ the sequence is empty.
* If $M$ is a countable model of $\overline{\mathsf{ZF}}$ in which the sequence is $s$ and $t \in M$ is a finite sequence extending $s$ then there is an end-extension $N \models \overline{\mathsf{ZF}}$ of $M$ in which the sequence is exactly $t$.
* Indeed, for the previous statements it suffices that $M \models \mathsf{ZF}$ and end-extends a submodel $W \models \overline{\mathsf{ZF}}$ of height at least $(\omega_1^{\mathrm{L}})^M$.

This universal finite sequence can be used to determine the modal validities of end-extensional set-theoretic potentialism, namely to be exactly the modal theory $\mathsf{S4}$. The sequence can also be used to show that every countable model of set theory extends to a model satisfying the end-extensional maximality principle, asserting that any possibly necessary sentence is already true.

This talk is about joint work with Joel David Hamkins. The $\Sigma_1$ universal finite sequence is a sister to the $\Sigma_2$ universal finite sequence for rank-extensions of Hamkins and Woodin, and both are cousins of Woodin's universal algorithm for arithmetic.

Video

​

Cofinal extensions generally preserve many more properties of a model of arithmetic than their sisters, end extensions. Exactly how much must or can they preserve? The answer is intimately related to how much arithmetic the model can do. I will survey what is known and what is not known about this question, and report on some recent work on this line.

Slides

Video

In the context of arithmetic, a reflection principle for a theory Th is a formal way of expressing that all theorems of Th are true. In the presence of a truth predicate for the language of Th this principle can be expressed as a single sentence (called the Global Reflection principle over Th) but most often is met in the form of a scheme consisting of all sentences of the form

$\forall x \bigl( \text{Prov}_{\text{Th}}(\phi(\dot{x}))\rightarrow \phi(x)\bigr).$ Obviously such a scheme is not provable in a consistent theory Th. Nevertheless, such soundness assertions are said to provide a natural and justified way of extending ones initial theory.

This perspective is nowadays very fruitfully exploited in the context of formal theories of truth. One of the most basic observations is that strong axioms for the notions of truth follow from formally weak types of axiomatizations modulo reflection principles. In such a way compositional axioms are consequences of the uniform disquotational scheme for for the truth predicate, which is

$\forall x\, \, T(\phi(\dot{x}))\equiv \phi(x).$

The above observation is also used in the recent approach to ordinal analysis of theories of predicative strength by Lev Beklemishev and Fedor Pakhomov. The assignment of ordinal notations to theories proceeds via partial reflection principles (for formulae of a fixed $\Sigma_n$ complexity) over (iterated) disquotational scheme. It becomes important to relate theories of this form to fragments of standard theories of truth, in particular the ones based on induction for restricted classes of formulae such as $\text{CT}_0$ (the theory of compositional truth with $\Delta_0$-induction for the extended language. The theory was discussed at length in Bartek Wcisło's talk). Beklemishev and Pakhomov leave the following open question:

Is $\Sigma_1$-reflection principle over the uniform disquotational scheme provable in $\text{CT}_0$?

The main goal of our talk is to present the proof of the affirmative answer to this question. The result significantly improves the known fact on the provability of Global Reflection over PA in $\text{CT}_0$. During the talk, we explain the theoretical context described above including the information on how the result fits into Beklemishev-Pakhomov project. In the meantime we give a different proof of their characterisation of $\Delta_0$-reflection over the disquotational scheme.

Despite the proof-theoretical flavour of these results, our proofs rests on essentially model-theoretical techniques. The important ingredient is the Arithmetized Completeness Theorem.

Slides

Video

​

A Kaufmann model is an $\omega_1$-like, recursively saturated, rather classless model of PA. Such models were constructed by Kaufmann under the $\diamondsuit$ assumption and then shown to exist in ZFC by Shelah using an absoluteness argument involving the logic $L_{\omega_1, \omega}(Q)$ where $Q$ is the quantifier 'there exists uncountably many…'. It remains an intriguing, if vague, open problem whether one can construct a Kaufmann model in ZFC 'by hand' i.e. without appealing to some form of absoluteness or other very non-constructive methods. In this talk I consider the related problem of axiomatizing Kaufmann models in $L_{\omega_1, \omega}(Q)$ and show that this is independent of ZFC. Along the way we'll see that it is also independent of ZFC whether there is an $\omega_1$-preserving forcing notion adding a truth predicate to a Kaufmann model.

Video

In the 1973 paper 'Countable models of set theory', H. Friedman's investigation of embeddings between countable models of subsystems of ZF yields the following two striking results:

1. Every countable nonstandard model of PA is isomorphic to a proper initial segment of itself.
2. Every countable nonstandard model of a sufficiently strong subsystem of ZF is isomorphic to a proper initial segment that is a union of ranks of the original model.

Note that, in contrast to PA, in the context of set theory there are three alternative notions of 'initial segment': transitive subclass, transitive subclass that is closed under subsets and rank-initial segment. Paul Gorbow, in his Ph.D. thesis, systematically studies versions of H. Friedman's self-embedding that yield isomorphisms between a countable nonstandard model of set theory and a rank-initial segment of itself. In these two talks I will discuss recent joint work with Ali Enayat that investigates models of set theory that are isomorphic to a transitive subclass of itself. We call the maps witnessing these isomorphisms 'initial self-embeddings'. I will outline a proof of a refinement of H. Friedman's Theorem that guarantees the existence of initial self-embeddings for certain subsystems of ZF without the powerset axiom. I will then discuss several examples including a nonstandard model of ZFC minus the powerset axiom that admits no initial self-embedding, and models that separate the three different notions of self-embedding for models of set theory. Finally, I will discuss two interesting applications of our version of H. Freidman's Theorem. The first of these is a refinement of a result due to Quinsey that guarantees the existence of partially elementary proper transitive subclasses of non-standard models of ZF minus the powerset axiom. The second result shows that every countable model of ZF with a nonstandard natural number is isomorphic to a transitive subclass of the hereditarily countable sets of its own constructible universe.​

Slides

Video

Truth theories investigate the notion of truth using axiomatic methods. To a fixed base theory (typically Peano Arithmetic ${\rm PA}$) we add a unary predicate $T(x)$ with the intended interpretation '$x$ is a (code of a) true sentence.' Then we analyse how adding various possible sets of axioms for that predicate affects its behaviour.

One of the aspects which we are trying to understand is which truth-theoretic principles make the added truth predicate 'strong' in that the resulting theory is not conservative over the base theory. Ali Enayat proposed to call this demarcating line between conservative and non-conservative truth theories 'the Tarski boundary.'

Research on Tarski boundary revealed that natural truth theoretic principles extending compositional axioms tend to be either conservative over ${\rm PA}$ or exactly equivalent to the principle of global reflection over $
A$. It says that sentences provable in ${\rm PA}$ are true in the sense of the predicate $T$. This in turn is equivalent to $\Delta_0$ induction for the compositional truth predicate which turns out to be a surprisingly robust theory.

The equivalences between nonconservative truth theories are typically proved by relatively direct ad hoc arguments. However, certain patterns seem common to these proofs. The first one is construction of various arithmetical partial truth predicates which provably in a given theory have better properties than the original truth predicate. The second one is deriving induction for these truth predicates from internal induction, a principle which says that for any arithmetical formula, the set of those elements for which that formula is satisfied under the truth predicate satisfies the usual induction axioms.

As an example of this phenomenon, we will present two proofs. First, we will show that global reflection principle is equivalent to local induction. Global reflection expresses that any sentence provable in ${\rm PA}$ is true. Local induction says that any predicate obtained by restricting truth predicate to sentences of a fixed syntactic complexity $c$ satisfies full induction. This is an observation due to Mateusz Łełyk and the author of this presentation.

The second example is a result by Ali Enayat who showed that ${\rm CT}_0$, a theory compositional truth with $\Delta_0$ induction, is arithmetically equivalent to the theory of compositional truth together with internal induction and disjunctive correctness.

This talk is intended as a continuation of 'Tarski boundary II' presentation at the same seminar. However, we will try to avoid excessive assumptions on familiarity with the previous part.

Video

In the context of arithmetic, a reflection principle for a theory Th is a formal way of expressing that all theorems of Th are true. In the presence of a truth predicate for the language of Th this principle can be expressed as a single sentence (called the Global Reflection principle over Th) but most often is met in the form of a scheme consisting of all sentences of the form

$\forall x \bigl( \text{Prov}_{\text{Th}}(\phi(\dot{x}))\rightarrow \phi(x)\bigr).$ Obviously such a scheme is not provable in a consistent theory Th. Nevertheless, such soundness assertions are said to provide a natural and justified way of extending ones initial theory.

This perspective is nowadays very fruitfully exploited in the context of formal theories of truth. One of the most basic observations is that strong axioms for the notions of truth follow from formally weak types of axiomatizations modulo reflection principles. In such a way compositional axioms are consequences of the uniform disquotational scheme for for the truth predicate, which is

$\forall x\, \, T(\phi(\dot{x}))\equiv \phi(x).$

The above observation is also used in the recent approach to ordinal analysis of theories of predicative strength by Lev Beklemishev and Fedor Pakhomov. The assignment of ordinal notations to theories proceeds via partial reflection principles (for formulae of a fixed $\Sigma_n$ complexity) over (iterated) disquotational scheme. It becomes important to relate theories of this form to fragments of standard theories of truth, in particular the ones based on induction for restricted classes of formulae such as $\text{CT}_0$ (the theory of compositional truth with $\Delta_0$-induction for the extended language. The theory was discussed at length in Bartek Wcisło's talk). Beklemishev and Pakhomov leave the following open question:

Is $\Sigma_1$-reflection principle over the uniform disquotational scheme provable in $\text{CT}_0$?

The main goal of our talk is to present the proof of the affirmative answer to this question. The result significantly improves the known fact on the provability of Global Reflection over PA in $\text{CT}_0$. During the talk, we explain the theoretical context described above including the information on how the result fits into Beklemishev-Pakhomov project. In the meantime we give a different proof of their characterisation of $\Delta_0$-reflection over the disquotational scheme.

Despite the proof-theoretical flavour of these results, our proofs rests on essentially model-theoretical techniques. The important ingredient is the Arithmetized Completeness Theorem.

Slides

Video

​

In the 1973 paper 'Countable models of set theory', H. Friedman's investigation of embeddings between countable models of subsystems of ZF yields the following two striking results:

1. Every countable nonstandard model of PA is isomorphic to a proper initial segment of itself.
2. Every countable nonstandard model of a sufficiently strong subsystem of ZF is isomorphic to a proper initial segment that is a union of ranks of the original model.

Note that, in contrast to PA, in the context of set theory there are three alternative notions of 'initial segment': transitive subclass, transitive subclass that is closed under subsets and rank-initial segment. Paul Gorbow, in his Ph.D. thesis, systematically studies versions of H. Friedman's self-embedding that yield isomorphisms between a countable nonstandard model of set theory and a rank-initial segment of itself. In these two talks I will discuss recent joint work with Ali Enayat that investigates models of set theory that are isomorphic to a transitive subclass of itself. We call the maps witnessing these isomorphisms 'initial self-embeddings'. I will outline a proof of a refinement of H. Friedman's Theorem that guarantees the existence of initial self-embeddings for certain subsystems of ZF without the powerset axiom. I will then discuss several examples including a nonstandard model of ZFC minus the powerset axiom that admits no initial self-embedding, and models that separate the three different notions of self-embedding for models of set theory. Finally, I will discuss two interesting applications of our version of H. Freidman's Theorem. The first of these is a refinement of a result due to Quinsey that guarantees the existence of partially elementary proper transitive subclasses of non-standard models of ZF minus the powerset axiom. The second result shows that every countable model of ZF with a nonstandard natural number is isomorphic to a transitive subclass of the hereditarily countable sets of its own constructible universe.​

Truth theories investigate the notion of truth with axiomatic methods. To a fixed base theory (typically Peano Arithmetic ${\rm PA}$) we add a unary predicate $T(x)$ with the intended interpretation '$x$ is a (code of a) true sentence.' Then we analyse how adding various possible sets of axioms for that predicate affects its behaviour.

One of the aspects we are trying to understand is which truth-theoretic principles make the added truth predicate 'strong' in that the resulting theory is not conservative over the base theory. Ali Enayat proposed to call this 'demarcating line' between conservative and non-conservative truth theories 'the Tarski boundary.'

Research on Tarski boundary revealed that natural truth theoretic principles extending compositional axioms tend to be either conservative over ${\rm PA}$ or exactly equivalent to the principle of global reflection over ${\rm PA}$. It says that sentences provable in ${\rm PA}$ are true in the sense of the predicate $T$. This in turn is equivalent to $\Delta_0$ induction for the compositional truth predicate which turns out to be a surprisingly robust theory.

In our talk, we will try to sketch proofs representative of research on Tarski boundary. We will present the proof by Enayat and Visser showing that the compositional truth predicate is conservative over ${\rm PA}$. We will also try to discuss how this proof forms a robust basis for further conservativeness results.

On the non-conservative side of Tarski boundary, the picture seems less organised, since more arguments are based on ad hoc constructions. However, we will try to show some themes which occur rather repeatedly in these proofs: iterated truth predicates and the interplay between properties of good truth-theoretic behaviour and induction. To this end, we will present the argument that disjunctive correctness together with the internal induction principle for a compositional truth predicate yields the same consequences as $\Delta_0$-induction for the compositional truth predicate (as proved by Ali Enayat) and that it shares arithmetical consequences with global reflection. The presented results are currently known to be suboptimal.

This talk is intended as a continuation of 'Tarski boundary' presentation. However, we will try to avoid excessive assumptions on familiarity with the previous part.

There is a well-known close logical connection between PA and finite set theory. Is there a set theory that corresponds in an analogous way to bounded arithmetic $I\Delta_0$? I propose a candidate for such a theory, called $I\Delta_0S$, and consider the questions: what set-theoretic axioms can it prove? And given a model M of $I\Delta_0$ is there a model of $I\Delta_0S$ whose ordinals are isomorphic to M? The answer is yes if M is a model of Exp; to obtain the answer we use a new way of coding sets by numbers.

Slides

The subject of this two-part talk is a 1975 Barwise-Schlipf landmark paper, whose main theorem asserts that a nonstandard model M of PA is recursively saturated iff M has an expansion to a model of the subsystem $\Delta^{1}_{1}-CA_0$ of second order arithmetic. The impression one gets from reading the Barwise-Schlipf paper is that the left-to-right direction of the theorem is deep since it relies on sophisticated techniques from admissible set theory, and that the other direction is fairly routine.

As it turns out, the exact opposite is the case: the left-to-right direction of the Barwise-Schlipf theorem lends itself to a proof from first principles (as observed independently by Jonathan Stavi and Sol Feferman not long after the appearance of the Barwise-Schmerl paper); and moreover, as recently shown in my joint work with Jim Schmerl, there is a crucial error in the Barwise-Schlipf proof of the right-to-left direction of the theorem, an error that can be circumvented by a rather nontrivial argument. As I will explain, certain results from the joint work of Matt Kaufmann and Jim Schmerl in the mid-1980s on 'lofty' models of arithmetic come in handy for the analysis of the error, and for circumventing it.

In part I, after going over some history, and preliminaries, I will discuss (1) the gap in the Barwise-Schlipf paper, and (2) the aforementioned Feferman-Stavi proof. In part II, I will focus on how the gap can be circumvented with a proof strategy very different from that Barwise and Schlipf.​

Slides

​

The subject of this two-part talk is a 1975 Barwise-Schlipf landmark paper, whose main theorem asserts that a nonstandard model M of PA is recursively saturated iff M has an expansion to a model of the subsystem $\Delta^{1}_{1}-CA_0$ of second order arithmetic. The impression one gets from reading the Barwise-Schlipf paper is that the left-to-right direction of the theorem is deep since it relies on sophisticated techniques from admissible set theory, and that the other direction is fairly routine.

As it turns out, the exact opposite is the case: the left-to-right direction of the Barwise-Schlipf theorem lends itself to a proof from first principles (as observed independently by Jonathan Stavi and Sol Feferman not long after the appearance of the Barwise-Schmerl paper); and moreover, as recently shown in my joint work with Jim Schmerl, there is a crucial error in the Barwise-Schlipf proof of the right-to-left direction of the theorem, an error that can be circumvented by a rather nontrivial argument. As I will explain, certain results from the joint work of Matt Kaufmann and Jim Schmerl in the mid-1980s on 'lofty' models of arithmetic come in handy for the analysis of the error, and for circumventing it.

In part I, after going over some history, and preliminaries, I will discuss (1) the gap in the Barwise-Schlipf paper, and (2) the aforementioned Feferman-Stavi proof. In part II, I will focus on how the gap can be circumvented with a proof strategy very different from that Barwise and Schlipf.​

Slides

​

Recall that given a complete theory $T$ and a type $p(x)$ the Hanf number for $p(x)$ is the least cardinal $\kappa$ so that any model of $T$ of size $\kappa$ realizes $p(x)$ (if such a $\kappa$ exists and $\infty$ otherwise). The Hanf number for $T$, denoted $H(T)$, is the supremum of the successors of the Hanf numbers for all possible types $p(x)$ whose Hanf numbers are $\lt\infty$. We have seen so far in the seminar that for any complete, consistent $T$ in a countable language $H(T) \leq \beth_{\omega_1}$ (a result due to Morley). In this talk I will present the following theorems: (1) The Hanf number for true arithmetic is $\beth_{\omega}$ (Abrahamson-Harrington-Knight) but (2) the Hanf number for False Arithmetic is $\beth_{\omega_1}$ (Abrahamson-Harrington)

PA is the first order fragment of Peano's axiomatization of the natural numbers. The natural numbers, N, is called the standard model of PA. But by compactness theorem in first order logic, there are also models of PA different from N, which are called non-standard models of arithmetic. Like in N, every element of a non-standard model M has a binary expansion, which can be regarded as the characteristic function of a subset of N. The standard system of M is the collection of all such subsets of N. It is known that standard systems of non-standard models are always Scott sets and every Scott set of cardinality less than or equal to the first uncountable cardinal is the standard system of some non-standard model. However, the general Scott set problem, whether every Scott set is the standard system of some non-standard model, remains one of the major open problems in the model theory of arithmetic. This talk will present some history of Scott set problem, as well as two constructions of non-standard models with uncountable standard systems.

Slides

When $A \subseteq \mathcal{M} \vDash PA^{\ast}$, we say that $A$ is a basis for $\mathcal{M}$ if for all $X \subseteq A$, the submodel $M_{X}$ generated by $X$ is the unique $\mathcal{N} \prec \mathcal{M}$ such that $X = \mathcal{N} \cap A$, and that such $A$ is solid if for all finite $X,Y \subseteq A$, whenever $f: \mathcal{M}_{X} \to \mathcal{M}_{Y}$ is an isomorphism, then $f \upharpoonright_{X}$ is one-to-one onto $Y$. We will discuss what role a solid basis can play in controlling the amount of indiscernibility and the automorphisms of a model. Also, using a set of types called an 'AH-set', we will construct a solid basis.

In this talk, we will review Morley's 1963 article 'Omitting Classes of Elements' (in modern parlance, omitting types). In this paper, Morley investigates the question of how large a structure's cardinality must be before it is forced to realize a type (for example, an ordered field with cardinality greater than the continuum must contain non-Archimedean elements). Given a fixed language, there is a cardinal $\kappa$ such that for every theory $T$ and any type $\Sigma$, if $T$ has a model of size $\kappa$ omitting $\Sigma$ then it has such a model in every cardinality. Morley's main result is that given a countable language $L$, if for every $\alpha < \omega_1$ there is a model of $T$ of size $\geq \beth_\alpha$ which omits $\Sigma$, then there is such a model in every cardinality (and if $L$ has at most $\aleph_\beta$ symbols, we replace '$\omega_1$' in this statement by '$\omega_{\gamma + 1}$' where $2^{\aleph_\beta} = \aleph_\gamma$). The proof uses the Erdős–Rado partition theorem and indiscernible sequences.

I will continue to speak about the construction in Jim Schmerl's paper on the pentagon lattice.

The goal of Gödel’s argument that the theory (T) of Peano Arithmetic is not complete, was to show that the Gödel sentences, $G$ , and it’s negation, are not provable in T, unless T is inconsistent. In this paper we examine the first half of this argument, namely, that from a hypothetical derivation, $P_{G}$, of $G$, a derivation, $P_{f}$, can be constructed that ends in a contradiction. We make the observation that the Gödel argument depends on the metatheory concept of representability that, in turn, depends on the metatheory concept of soundness. Our analysis leads to two main observations, the first well know, and the second, a challenge to the standard undecidability argument.

1 – The existence of $P_G$ implies that T is unsound. This conclusion does not require the further construction, from $P_G$, of the derivation $P_f$.

2 - We argue that effectuation of the construction of $P_f$ is obstructed, because that effectuation requires acceptance of a contradiction in the metatheory regarding the soundness of T.

This is joint work with Catherine Hennix.

I will continue to speak about Jim Schmerl's recent paper on the pentagon lattice $\mathbf{N}_5$. In this talk, I will outline the main result that no model of PA has a 'mixed' elementary extension such that the resulting interstructure lattice is isomorphic to the pentagon.