Fredrik Engström

First, we describe a psychological experiment in which the participants were asked to determine whether sentences of first-order logic were true or false in finite graphs. Second, we define two proof systems for reasoning about truth and falsity in first-order logic. These proof systems feature explicit models of cognitive resources such as declarative memory, procedural memory, working memory, and sensory memory. Third, we describe a computer program that is used to find the smallest proofs in the aforementioned proof systems when capacity limits are put on the cognitive resources. Finally, we investigate the correlation between a number of mathematical complexity measures defined on graphs and sentences and some psychological complexity measures that were recorded in the experiment

The dual character of invariance under transformations and definability by some operations has been used in classical works by, for example, Galois and Klein. Following Tarski, philosophers of logic have claimed that logical notions themselves could be characterized in terms of invariance. In this article, we generalize a correspondence due to Krasner between invariance under groups of permutations and definability in L∞∞ so as to cover the cases that are of interest in the logicality debates, getting McGee’s theorem about quantifiers invariant under all permutations and definability in pure L∞∞ as a particular case. We also prove some optimality results along the way, regarding the kinds of relations which are needed so that every subgroup of the full permutation group is characterizable as a group of automorphisms.

Let (M, X) ⊨ ACA₀ be such that P X, the collection of all unbounded sets in X, admits a definable complete ultrafilter and let T be a theory extending first order arithmetic coded in X such that M thinks T is consistent. We prove that there is an end-extension N ⊨ T of M such that the subsets of M coded in N are precisely those in X. As a special case we get that any Scott set with a definable ultrafilter coding a consistent theory T extending first order arithmetic is the standard system of a recursively saturated model of T

Recursive saturation and resplendence are two important notions in models of arithmetic. Kaye, Kossak, and Kotlarski introduced the notion of arithmetic saturation and argued that recursive saturation might not be as rigid as first assumed. In this thesis we give further examples of variations of recursive saturation, all of which are connected with expandability properties similar to resplendence. However, the expandability properties are stronger than resplendence and implies, in one way or another, that the expansion not only satisfies a theory, but also omits a type. We conjecture that a special version of this expandability is in fact equivalent to arithmetic saturation. We prove that another of these properties is equivalent to -saturation. We also introduce a variant on recursive saturation which makes sense in the context of a standard predicate, and which is equivalent to a certain amount of ordinary saturation. The theory of all models which omit a certain type p(¯x) is also investigated. We define a proof system, which proves a sentence if and only if it is true in all models omitting the type p(¯x). The complexity of such proof systems are discussed and some explicit examples of theories and types with high complexity, in a special sense, are given. We end the thesis by a small comment on Scott’s problem. The problem is to characterise standard systems of models of arithmetic. We prove that, under the assumption of Martin’s axiom, every Scott set of cardinality < 2@0 closed under arithmetic comprehension which has the countable chain condition is the standard system of some model of PA. However, we do not know if there exists any such uncountable Scott sets.

We introduce generalized quantifiers, as defined in Tarskian semantics by Mostowski and Lindström, in logics whose semantics is based on teams instead of assignments, e.g., IF-logic and Dependence logic. Both the monotone and the non-monotone case is considered. It is argued that to handle quantifier scope dependencies of generalized quantifiers in a satisfying way the dependence atom in Dependence logic is not well suited and that the multivalued dependence atom is a better choice. This atom is in fact definably equivalent to the independence atom recently introduced by Väänänen and Grädel