Easy Proofs of L\"owenheim-Skolem Theorems by Means of Evaluation Games

TL;DR

This paper introduces a simpler, game-theoretic proof of the downward L"owenheim-Skolem theorem that enhances understanding and teaching of first-order logic semantics.

Contribution

It presents a novel proof method based on evaluation games, avoiding Skolem normal forms, making the proof more accessible for students.

Findings

Proof is simpler and more intuitive for students.

Uses evaluation games to establish the theorem.

Avoids complex Skolemization process.

Abstract

We propose a proof of the downward L\"owenheim-Skolem that relies on strategies deriving from evaluation games instead of the Skolem normal forms. This proof is simpler, and easily understood by the students, although it requires, when defining the semantics of first-order logic to introduce first a few notions inherited from game theory such as the one of an evaluation game.