这里是如何引入一个有意义的公理（我自己还在学习Coq，所以如果我做错了，希望有人能纠正我）。
使用
Parameter，我们规定了一个名为
compute的函数的存在，但没有给出定义。使用
Axiom，我们确定了它的一些属性（希望不会引入矛盾）。据说，参数和公理在内部执行相同的操作。
类似于
compute的声明，您的公理Phi规定了从
nat到
partial的函数Phi的存在，但是在
Coq中您无法对其进行任何操作，因为它没有已知的属性。请注意，Phi的存在并不意味着“存在可部分计算函数的有效枚举”。
这里的公理表明，在允许更多步骤的计算时，
compute永远不会将ACCEPT更改为REJECT或反之亦然，也不会回退到NOTYET。通过这些定义，我已经检查过可以证明一个简单的引理
test作为起点。
显然，我没有进行下去以查看是否可以证明停机问题的不可判定性，但是通过添加一个公理来断言存在一个
nat，表示与停机问题证明所需构造等效的程序，应该是可能的。当然，通过这种方式做事情，基本上证明的全部意义都失去了，但仍然有一点需要证明。
Inductive result :=
| ACCEPT : result
| REJECT : result
| NOTYET : result.
Definition narrowing a b : Prop :=
(match a with
| ACCEPT => b = ACCEPT
| REJECT => b = REJECT
| NOTYET => True
end).
Parameter compute : nat (* program *) -> nat (* argument *) -> nat (* steps *) -> result.
Axiom compute_narrowing:
forall program input steps steps',
(steps' >= steps) ->
(narrowing (compute program input steps) (compute program input steps')).
Lemma test: ~ exists program input steps, (compute program input steps) = ACCEPT /\ (compute program input (steps + 1)) = NOTYET
编辑：这里有更多内容。经过一番思考，我意识到我肯定是错的，认为这样的证明必须公理化有趣的构造。人们可以插入仅允许简单低级构造并在其上构建更高级别构造的公理。我假设目标是遵循明斯基的证明，因为它似乎更容易形式化：
http://www.cs.odu.edu/~toida/nerzic/390teched/computability/unsolv-1.html。
在这里，额外的公理断言1）存在一个始终接受的程序2）存在一个始终拒绝的程序3）对于任何三个程序条件语句 当接受时 当拒绝时，存在一个程序首先运行条件语句，然后基于此运行当接受时或当拒绝时（所有子程序调用都在给定给组合程序的相同输入上进行）。有了这些公理，就可以证明对于任何程序目标，存在一个程序运行目标，然后输出相反的结果（但如果目标永远循环，则也会永远循环）。这个“否定”构造只是一个简单的例子，而不是明斯基证明中使用的构造之一。
要遵循明斯基的证明，需要添加进一步公理以存在一个循环程序和复制机构造。然后添加一个定义，当一个程序是一个决策者时，并证明不存在一个决策者来解决停机问题。codec公理可以避免在Coq中定义函数encode_pair和decode_pair并将codec证明为引理。我认为encode_pair和decode_pair的属性将需要在复制机构造和最终证明中使用（当然，停机问题的决策者定义将需要它，因为机器输入是一对）。
Require Import List.
Require Import Arith.
Require Import Omega.
Ltac mp_cancel :=
repeat match goal with
| [ H2 : ?P -> ?Q , H1 : ?P |- _ ] => specialize (H2 H1)
end.
Ltac mp_cancel_reflexivity :=
repeat match goal with
| [ H1 : ?P = ?P -> ?Q |- _ ] => assert (H_mp_cancel_reflexivity : P = P) by reflexivity; specialize (H1 H_mp_cancel_reflexivity); clear H_mp_cancel_reflexivity
end.
Inductive result :=
| ACCEPT : result
| REJECT : result
| NOTYET : result
.
Definition narrowing a b : Prop :=
(match a with
| ACCEPT => b = ACCEPT
| REJECT => b = REJECT
| NOTYET => True
end)
.
Parameter encode_pair : (nat * nat) -> nat.
Parameter decode_pair : nat -> (nat * nat).
Axiom codec:
forall a b,
(decode_pair (encode_pair (a, b))) = (a, b).
Parameter compute : nat (* program *) -> nat (* input *) -> nat (* steps *) -> result.
Axiom compute_narrowing:
forall program input steps steps',
(steps' >= steps) -> (narrowing (compute program input steps) (compute program input steps')).
Axiom exists_always_accept:
exists program_always_accept,
forall input,
exists steps,
(compute program_always_accept input steps) = ACCEPT.
Axiom exists_always_reject:
exists program_always_reject,
forall input,
exists steps,
(compute program_always_reject input steps) = REJECT.
Definition result_compose_conditional (result_conditional : result) (result_when_accept : result) (result_when_reject : result) : result :=
(match result_conditional with
| ACCEPT => result_when_accept
| REJECT => result_when_reject
| NOTYET => NOTYET
end).
Axiom exists_compose_conditional:
forall program_conditional program_when_accept program_when_reject,
exists program_composition,
forall input steps_control steps_when result_conditional result_when_accept result_when_reject,
(
((compute program_conditional input steps_control) = result_conditional) ->
((compute program_when_accept input steps_when) = result_when_accept) ->
((compute program_when_reject input steps_when) = result_when_reject) ->
(exists steps_composition, (compute program_composition input steps_composition) = (result_compose_conditional result_conditional result_when_accept result_when_reject))
).
Definition result_negation (result_target : result) : result :=
(match result_target with
| ACCEPT => REJECT
| REJECT => ACCEPT
| NOTYET => NOTYET
end).
Lemma exists_negation:
forall program_target,
exists program_negation,
forall input steps_target result_target,
(
((compute program_target input steps_target) = result_target) ->
(exists steps_negation, (compute program_negation input steps_negation) = (result_negation result_target))
).
intros.
elim exists_always_accept; intros program_always_accept H_always_accept.
elim exists_always_reject; intros program_always_reject H_always_reject.
elim exists_compose_conditional with (program_conditional := program_target) (program_when_accept := program_always_reject) (program_when_reject := program_always_accept); intros program_negation H_program_negation.
exists program_negation.
intros.
specialize H_always_accept with input. elim H_always_accept; clear H_always_accept; intros steps_accept H_always_accept.
specialize H_always_reject with input. elim H_always_reject; clear H_always_reject; intros steps_reject H_always_reject.
pose (steps_when := (steps_accept + steps_reject)).
specialize H_program_negation with input steps_target steps_when result_target (compute program_always_reject input steps_when) (compute program_always_accept input steps_when).
mp_cancel.
mp_cancel_reflexivity.
elim H_program_negation; clear H_program_negation; intros steps_negation H_program_negation.
exists (steps_negation).
rewrite H_program_negation; clear H_program_negation.
replace (compute program_always_reject input steps_when) with REJECT; symmetry.
replace (compute program_always_accept input steps_when) with ACCEPT; symmetry.
unfold result_compose_conditional.
unfold result_negation.
reflexivity.
assert (T := (compute_narrowing program_always_accept input steps_accept steps_when)).
assert (steps_when >= steps_accept).
unfold steps_when.
omega.
mp_cancel.
unfold narrowing in T.
rewrite H_always_accept in T.
assumption.
assert (T := (compute_narrowing program_always_reject input steps_reject steps_when)).
assert (steps_when >= steps_reject).
unfold steps_when.
omega.
mp_cancel.
unfold narrowing in T.
rewrite H_always_reject in T.
assumption.
Qed.
编辑#2：我有点理解你想要能够在Coq中编程构造，但我之前的编辑时还没有想出如何做到。在下面的代码片段中，使用公理
exists_program_of_procedure来完成，该公理断言存在一个表示程序的
nat，其行为与任何给定的过程相同（至少对于计算“缩小”的良好过程）。包括Minsky证明的直接形式化。您的方法肯定具有更简洁的公理，并且由于使用
modulus将步骤转换为预测器而不是处理
narrowing，因此可能会导致更短的证明。最有趣的是看看您的方法是否可以在不使用
Classical的情况下执行。
更新：似乎您的公理引入了一个矛盾，因为
modulus不应该是可计算的（？）。
Require Import List.
Require Import Arith.
Require Import Omega.
Ltac mp_cancel :=
repeat match goal with
| [ H2 : ?P -> ?Q , H1 : ?P |- _ ] => specialize (H2 H1)
end.
Ltac mp_cancel_reflexivity :=
repeat match goal with
| [ H1 : ?P = ?P -> ?Q |- _ ] => assert (H_mp_cancel_reflexivity : P = P) by reflexivity; specialize (H1 H_mp_cancel_reflexivity); clear H_mp_cancel_reflexivity
end.
Parameter encode_pair: (nat * nat) -> nat.
Parameter decode_pair: nat -> (nat * nat).
Axiom decode_encode: forall a b, (decode_pair (encode_pair (a, b))) = (a, b).
Inductive result :=
| ACCEPT : result
| REJECT : result
| NOTYET : result.
Definition result_narrowing (a : result) (b : result) : Prop :=
(match a with
| ACCEPT => b = ACCEPT
| REJECT => b = REJECT
| NOTYET => True
end).
Lemma result_narrowing_trans: forall a b c, result_narrowing a b -> result_narrowing b c -> result_narrowing a c.
intros until 0.
destruct a; destruct b; destruct c;
unfold result_narrowing;
intros;
try discriminate;
reflexivity.
Qed.
Parameter compute: nat (* program *) -> nat (* input *) -> nat (* steps *) -> result.
Axiom compute_narrowing:
forall program input steps steps',
(steps' >= steps) -> (result_narrowing (compute program input steps) (compute program input steps')).
Require Import Classical.
Lemma compute_non_divergent:
forall program input steps steps',
(compute program input steps) = ACCEPT ->
(compute program input steps') = REJECT ->
False.
intros.
assert (T := (classic (steps' >= steps))).
destruct T.
assert (T := (compute_narrowing program input steps steps')).
mp_cancel.
rewrite H, H0 in T.
unfold result_narrowing in T.
discriminate T.
unfold not in H1.
assert (T := (classic (steps' = steps))).
destruct T.
rewrite H2 in H0.
rewrite H in H0.
discriminate.
assert (steps >= steps').
omega.
assert (T := (compute_narrowing program input steps' steps)).
mp_cancel.
rewrite H, H0 in T.
unfold result_narrowing in T.
discriminate.
Qed.
Definition procedure_type := nat (* input *) -> nat (* depth *) -> result.
Definition procedure_narrowing (procedure : procedure_type) : Prop :=
forall input depth depth',
(depth' >= depth) -> (result_narrowing (procedure input depth) (procedure input depth')).
Axiom exists_program_of_procedure:
forall procedure : procedure_type,
(procedure_narrowing procedure) ->
exists program,
forall input,
(
forall depth,
exists steps,
(result_narrowing (procedure input depth) (compute program input steps))
) /\
(
forall steps,
exists depth,
(result_narrowing (compute program input steps) (procedure input depth))
).
Definition program_halts_on_input (program : nat) (input : nat) : Prop :=
(exists steps, (compute program input steps) <> NOTYET).
Definition program_is_decider (program : nat) : Prop :=
forall input,
exists steps,
(compute program input steps) <> NOTYET.
Definition program_solves_halting_problem_partially (program : nat) : Prop :=
forall input,
forall steps,
(
((compute program input steps) = ACCEPT)
-> (match (decode_pair input) with | (target_program, target_input) => ( (program_halts_on_input target_program target_input)) end)
) /\
(
((compute program input steps) = REJECT)
-> (match (decode_pair input) with | (target_program, target_input) => (~ (program_halts_on_input target_program target_input)) end)
).
Lemma minsky: (~ (exists halts, (program_is_decider halts) /\ (program_solves_halting_problem_partially halts))).
unfold not.
intros H_ph.
elim H_ph; clear H_ph; intros invocation_halts [H_ph_d H_ph_b].
pose
(procedure_modified := (fun (input : nat) (depth : nat) =>
(match (compute invocation_halts input depth) with
| ACCEPT => NOTYET
| REJECT => REJECT
| NOTYET => NOTYET
end))).
pose
(procedure_wrapper := (fun (input : nat) (depth : nat) =>
(procedure_modified (encode_pair (input, input)) depth))).
unfold procedure_modified in procedure_wrapper.
clear procedure_modified.
assert (T1 := (exists_program_of_procedure procedure_wrapper)).
assert (T2 : (procedure_narrowing procedure_wrapper)).
{
clear T1.
unfold procedure_narrowing, procedure_wrapper.
intros.
unfold result_narrowing.
case_eq (compute invocation_halts (encode_pair (input, input)) depth); try intuition.
assert (T := (compute_narrowing invocation_halts (encode_pair (input, input)) depth depth')).
mp_cancel.
rewrite H0 in T.
unfold result_narrowing in T.
rewrite T.
reflexivity.
}
mp_cancel.
clear T2.
elim T1; clear T1; intros program_wrapper H_pw.
unfold procedure_wrapper in H_pw.
clear procedure_wrapper.
specialize (H_pw program_wrapper).
destruct H_pw as [H_pw_fwd H_pw_rev].
unfold program_is_decider in H_ph_d.
specialize (H_ph_d (encode_pair (program_wrapper, program_wrapper))).
elim H_ph_d; clear H_ph_d; intros steps_inner H_ph_d.
unfold program_solves_halting_problem_partially in H_ph_b.
specialize (H_ph_b (encode_pair (program_wrapper, program_wrapper)) steps_inner).
destruct H_ph_b as [H_ph_b_1 H_ph_b_2].
case_eq (compute invocation_halts (encode_pair (program_wrapper, program_wrapper)) steps_inner).
{
intros.
rewrite H in *.
mp_cancel_reflexivity.
unfold program_halts_on_input in H_ph_b_1.
rewrite decode_encode in H_ph_b_1.
elim H_ph_b_1; clear H_ph_b_1; intros steps_outer H_ph_b_1.
specialize (H_pw_rev steps_outer).
case_eq (compute program_wrapper program_wrapper steps_outer).
{
intros.
rewrite H0 in *.
unfold result_narrowing in H_pw_rev.
elim H_pw_rev; clear H_pw_rev; intros depth H_pw_rev.
case_eq (compute invocation_halts (encode_pair (program_wrapper, program_wrapper)) depth); intros Hx; rewrite Hx in *; try discriminate.
}
{
intros.
rewrite H0 in *.
unfold result_narrowing in H_pw_rev.
elim H_pw_rev; clear H_pw_rev; intros depth H_pw_rev.
case_eq (compute invocation_halts (encode_pair (program_wrapper, program_wrapper)) depth); intros Hx; rewrite Hx in *; try discriminate.
assert (T := (compute_non_divergent invocation_halts (encode_pair (program_wrapper, program_wrapper)) steps_inner depth)).
mp_cancel.
assumption.
}
{
intros.
intuition.
}
}
{
intros.
rewrite H in *.
mp_cancel_reflexivity.
unfold not, program_halts_on_input in H_ph_b_2.
specialize (H_pw_fwd steps_inner).
rewrite H in H_pw_fwd.
unfold result_narrowing in H_pw_fwd.
elim H_pw_fwd; intros.
rewrite decode_encode in H_ph_b_2.
contradict H_ph_b_2.
exists x.
unfold not.
intros.
rewrite H0 in H1.
discriminate.
}
{
intros.
unfold not in H_ph_d.
mp_cancel.
assumption.
}
Qed.
