PaperlayerView exact revision on arXiv

Source-linked AI summary

Medvedev Logic is Not Decidable. It is {\pi}01 -complete. Who Would Have Guessed?

Pawel Pawlowski

arXiv:2609.11576v1cs.LOmath.LO

TL;DR

Whether Medvedev logic is decidable or recursively enumerablely axiomatizable had remained open. The paper connects finite Wang-system tilings to realizations of Wang–Medvedev pairs and then to finite Medvedev-frame refutations, establishing completeness under computable many-one reductions and its stated consequences.

  • Problem

    Whether ML is decidable or has a recursively enumerable axiomatization remained open.

    Source: §1 · p. 1

  • Method

    The paper encodes finite Wang systems as Wang–Medvedev pairs, proves their realizability equivalent to torus tiling, and translates realizability into a formula refutable on a finite Medvedev frame.

    Source: §1 · p. 2, §3 · p. 10, §4 · p. 16

  • Results

    The paper reports completeness under computable many-one reductions and concludes that ML is not recursively enumerable and has no recursively enumerable sound and complete proof calculus.

    Source: §1 · pp. 1–2

  • Takeaways & Limitations

    The result establishes that ML is undecidable and rules out a recursively enumerable sound and complete proof calculus.

    Source: §1 · pp. 1–2

    Response choices need not be unique; the argument establishes legality for each fixed choice.

    Source: §3 · p. 9

Abstract

from arXiv · show

This project began as an attempt to prove that Medvedev logic is decidable with the help of generative AI systems. The author (as well as the generative AI systems, or at least they claim to be since I have asked them) was surprised by its eventual conclusion. We prove that Medvedev logic ML, the intermediate logic of finite problems, is Pi-01-complete under computable many-one reductions. Consequently, ML is not recursively enumerable, a fortiori undecidable, and admits no recursively enumerable sound and complete proof calculus. The proof connects the periodic domino problem with intuitionistic formulas through a shared intermediate structure that we call a Wang-Medvedev pair. Such a pair consists of a finite partially ordered set of roles together with demands. Demands define the interaction between roles. A realization labels nonempty subsets of a finite set with these roles, respecting the order and satisfying the demands. We associate a pair with each finite Wang system and show that it has a realization iff the system tiles a finite torus. We then construct an intuitionistic formula that fails on some finite Medvedev frame iff the same pair is realizable. Realizability thus provides the link between periodic tilings and the countermodels.

1. Introduction

Medvedev logic is the intermediate logic of finite Medvedev frames, and its decidability and recursively enumerable axiomatizability had remained open. The paper connects periodic tilings to finite-frame countermodels to establish a completeness result and its consequences.

1. Introduction

  • Whether ML is decidable or has a recursively enumerable axiomatization remained open despite earlier results on its disjunction property and finite axiomatizability.The introduction also situates this work within results on structural completeness and fragments shared with intuitionistic logic.Source: §1 · p. 1
  • The paper reports completeness under computable many-one reductions, implying that ML is not recursively enumerable and has no recursively enumerable sound and complete proof calculus.The upper bound is by enumerating finite countermodels; the lower bound uses a translation from finite Wang systems to formulas.Source: §1 · pp. 1–2
  • A Wang–Medvedev pair links finite Wang systems to intuitionistic formulas: a finite torus tiling corresponds to realizability, which corresponds to a finite-frame refutation.The effective periodic domino theorem then connects finite torus tilings to machine halting.Source: §1 · p. 2
  • The paper develops the code and response-role table, proves both directions of the tiling equivalence, translates realizability into a formula, and assembles the complexity result.The construction direction carries most of the bookkeeping; proofs of opening lemmas and the response-role table are deferred to an appendix.Source: §1 · p. 2

2. The Wang system and its Wang–Medvedev code

The Wang–Medvedev code represents a finite Wang system with a role poset and demands, then asks whether nonempty subsets of a finite carrier can realize those roles. Its role supports and response rules encode cyclic coordinates, tile choices, and neighbour compatibility.

2. The Wang system and its Wang–Medvedev code

  • A Wang–Medvedev pair encodes a finite Wang system as a finite role poset with demands, and a realization labels nonempty carrier subsets subject to order and response requirements.Each demand requires a response subset of the union of its input sets whose role lies outside both input upsets.Source: §2 · pp. 3, 6
  • The column and row generator roles produce alternating cycles, while each cell response assigns a tile type to one column–row position.These cycles supply the torus indices; cell roles have four maximal roles used to compare neighbours.Source: §2 · p. 5, Figure 2 · p. 5, Figure 1 · p. 5
  • Source, step, expected, and candidate roles compare adjacent tile choices; forbidden pairs would require responses incompatible with coordinate containments.Provider roles and private keys supply auxiliary roles, and the vertical comparison exchanges the horizontal and vertical role names.Source: §2 · p. 5, Figure 3 · p. 6
  • The realization conditions require base and singleton roles, enforce containment according to the poset, and require responses for every pair of sets carrying demanded roles.A response may depend on its chosen input sets and need only lie in their union.Source: §2 · p. 6
  • Every role has a nonempty representative in a realization, and each role-bearing subset has exactly one role.A representative for a particular response must additionally satisfy the containment and response requirements.Source: §2 · p. 7
  • A response role must differ from both input roles, have support within their combined supports, and meet each input support; these tests are necessary, not sufficient.The forced response-role table lists exactly the admissible roles for each demanded pair, without guaranteeing a witness for every concrete input.Source: §2 · p. 7

3. From a finite realization to a torus tiling

A finite realization yields cyclic column and row indices, whose cell responses define a torus tile assignment. The construction proves that neighboring tiles satisfy both matching rules, including across the cyclic boundaries.

3. From a finite realization to a torus tiling

  • Column and row responses generate cycles; their lengths determine the torus dimensions and their positions supply cyclic indices.Each column set leads through a separator to the next column, and the row sets are constructed analogously.Source: §3 · pp. 8, 10
  • A response to each column–row pair has a unique cell role, defining the tile assignment at that position.The cell response is Cij = Resp(Pi, Vj), and its role determines the tile.Source: §3 · p. 9, Figure 4 · p. 9
  • For horizontal neighbors, a forbidden tile pair would require a response whose only permitted roles force impossible containments.The response would have to lie within a column separator or a row set, contradicting the distinct-role restrictions.Source: §3 · pp. 9–10
  • The vertical check rules out forbidden tile pairs by the same containment argument, using row separators and column sets.The resulting adjacent tiles therefore satisfy the vertical compatibility relation.Source: §3 · p. 10
  • Every finite realization of WM(D) yields a legal torus tiling, with positive periods that also cover the one-row or one-column cases.The column and row cycles give the periods, and the horizontal and vertical checks establish the tiling conditions.Source: §3 · p. 10

4. From a torus tiling to a finite realization

This section constructs a finite realization of WM(D) from a legal torus tiling, encoding positions and tile information in role-labelled sets. It gives the domain size and verifies the role conditions and demanded-state responses.

Construction from a torus tiling

  • The construction represents columns, rows, cells, seeds, and auxiliary states as subsets of K, with marker–maximal-role pairs and blocklists encoding coordinates and keys.Distinct missing symbols let unions test whether coordinates agree or are successive; barred states provide representatives for tiles absent from the tiling.Source: §4 · pp. 11–12

Sizes and exact supports

  • Each constructed set is a proper subset of K with at least two points, and its occurring maximal roles are exactly those in its prescribed support.Every supported block retains at least two points, while a maximal role outside the support witnesses properness.Source: §4 · p. 13

Separation of different roles

  • States assigned different intermediate roles yield incomparable sets, separating the role-labelled states used in the construction.The proof handles unequal supports and the special cases of column/row separators and cell states.Source: §4 · p. 13

Assigning the roles

  • The partial assignment satisfies (H0) and (H1): role prescriptions are consistent, and each assigned set contains representatives of exactly the roles above its own.The root contains representatives of every role, while each constructed intermediate-role set contains its own role and the maximal roles in its support.Source: §4 · pp. 13–14

Checking (H2)

  • For demanded pairs, responses encode cyclic column and row steps, combine column and row sets into cells, and use providers to supply tile-role responses.The same constructions cover actual cells and seed cells; step responses copy separator coordinates and obtain their private-key block from a provider.Source: §4 · p. 14
  • Expected–candidate demands use aligned-coordinate responses or mismatch responses, while forbidden tile-neighbour demands use the tiling’s legality to select a response.If a seed occurs, disjoint marker lists ensure the input union contains the whole next-column block, yielding the mismatch response.Source: §4 · p. 15

4. From a torus tiling to a finite realization

  • The seven families cover every demanded state pair, including seeds; legality excludes forbidden tile pairs at positions requiring adjacency in (D6) and (D7).For vertical (D7) cases, candidate choices make the relevant intersections empty, including the seed cases.Source: §4 · p. 16
  • Every legal m-by-n torus tiling of D yields a realization of WM(D) on K=J×MaxD, where |K|=(m+n+|T|+1)(4|T|+8).The construction verifies the realization conditions (H0)–(H2).Source: §4 · p. 16
  • For Mid-role sets X and Y forming a demand, the construction supplies a nonempty Ed subset of X∪Y whose role lies outside both upward role closures.This provides the response required for (H2).Source: §4 · p. 16

5. Recognizing a realization by a formula

The section translates a role-and-demand pair into an intuitionistic formula whose finite-frame countermodels correspond exactly to realizations. Traces and visible roles support both directions of this recognition, including on any fixed finite carrier.

5. Recognizing a realization by a formula

  • The formula α(P, D) uses clauses for role visibility, order, and demands to make a finite-frame refutation characterize realizability; its size is polynomial in |P|+|D|.The demand clause requires a visible role outside the two input upsets, representing a legal response.Source: §5 · p. 17
  • A trace records the roles represented by subsets of a world; every trace is a nonempty upset, is monotone under subset inclusion, and equals ↑λ on a set assigned role λ.The valuation makes eλ fail at X exactly when λ occurs in the trace of X.Source: §5 · p. 17
  • For each demand {λ, γ}, a response exists exactly when no world has trace ↑λ ∪ ↑γ.If equality held, there could be no response role outside the two input upsets; if it does not, a role in the trace difference supplies one.Source: §5 · p. 17
  • A realization yields a valuation refuting α(P, D), while a refutation yields a realization on its refuting world.The reverse construction assigns a role when the set of visible roles has the form ↑λ, using principalization to obtain subsets with required roles.Source: §5 · p. 18
  • For every finite nonempty K, F(K) refutes α(P, D) exactly when the pair has a realization on K.A realization recovered on a proper subset of K lifts to K along a surjection; if any finite realization exists, possible carrier sizes are all n ≥ n0 for some n0 ≥ 2.Source: §5 · p. 19

6. The complexity of Medvedev logic

The paper establishes Π0 1-completeness for Medvedev logic by reducing machine nonhalting through finite Wang systems and their recognizing formulas. Together with an effective search for finite countermodels, this yields undecidability and rules out recursively enumerable completeness.

6. The complexity of Medvedev logic

  • Membership in Π0 1 follows by enumerating finite Medvedev frames and halting when a valuation and world refute the input formula.Each stage checks finitely many persistent valuations and forcing conditions.Source: §6 · pp. 19–20
  • A computable construction maps each machine M to a finite Wang system DM that tiles a finite torus exactly when M halts on empty input.The construction pads the machine computation with two dummy transitions and converts tile colours into horizontal and vertical matching relations.Source: §6 · p. 20
  • Medvedev logic is 1-complete under computable many-one reductions; it is undecidable and not recursively enumerable, and admits no recursively enumerable sound and complete proof calculus.Source: §6 · pp. 20–21
  • The translation sends DM to αDM, with αDM in ML exactly when M does not halt on empty input.The formula is obtained by listing roles, supports, demands, and corresponding clauses.Source: §6 · pp. 20–21

Use of generative AI

The author describes generative AI as central to proof search and to the development of the tiling construction. The work began as an effort to prove decidability but shifted toward undecidability; the paper also reports a Lean formalization through Section 6.

Use of generative AI

  • Generative AI systems supplied initial construction ideas, proof sketches, and the use of tilings, and helped hone the construction.The author later reconstructed, revised, and clarified preliminary results.Source: Use of generative AI · p. 21
  • The project began by seeking a decidability proof, but partial results from AI-assisted dialogue suggested pursuing undecidability instead.The author reports a Lean formalization of the paper through Section 6, while noting that the halting-problem results were not reconstructed with AI assistance.Source: Use of generative AI · p. 21
  • Models including Fable, Sonnet, Opus, and ChatGPT 5.6 SOL were used for proof search, prompting, dialogue, source production, diagrams, and language improvement.The same models contributed to parts of the LaTeX source.Source: Use of generative AI · p. 21

Appendix A. Proofs of the opening lemmas and the response-role table

The appendix verifies the response-role table by testing which roles are legal responses to each demanded input pair. It also establishes structural facts about singleton roles, containment, and the form of actual responses.

Appendix A. Proofs of the opening lemmas and the response-role table

  • A response role must be distinct from the inputs, have support contained in the union of their supports, and intersect each input support.These tests determine admissible roles from the support table.Source: Appendix A · p. 22
  • For column and cell demands, the support tests yield unique responses: ColumnSep for (M1), Column for (M2), and cell roles for (M5).For (M6), the only admissible response to a projection role and its provider is that projection role.Source: Appendix A · p. 22
  • Axis exchange gives the corresponding row cases, including RowSep, Row, and RowStep, while the forbidden vertical tile-pair demand admits NotNextrow and NotSamecol.The support argument applies when (t, u) is not in V, without requiring H and V to be equal.Source: Appendix A · p. 23
  • The proof establishes that every actual response has one of the roles listed as admissible for its input pair.For a demanded pair, its response must be a Mid-role whose support is contained in the combined input supports and intersects both individual supports.Source: Appendix A · pp. 22–23
Loading 2609.11576v1…