“お膳立て”というより、証明そのものの話、しかも小ネタ。なのでオマケとします。
内容：
像と逆像に関する、とある命題
A, Bは集合、f:X→Y は写像、A⊆X, B⊆Y とします。このとき、次の命題は一般的には成立しません。
- f(f-1(B)) = B
f-1(B)は、Yの部分集合Bの逆像で、f(A)は、Xの部分集合Aの像〈順像〉です。
上記命題は成立しない、と言ったので、反例を挙げておきます。X = {1, 2}, Y = {1, 2, 3} として、f:{1, 2}→{1, 2, 3} を埋め込み写像として定義します。つまり、f(1) = 1, f(2) = 2。B = {2, 3} としたとき：
- f-1(B) = f-1({2, 3}) = {2}
- f(f-1(B)) = f({2}) = {2}
- {2} ≠ {2, 3}
もっと簡単な反例は、X = {1}, Y = B = {1, 2}, f(1) = 1, {1} ≠ {1, 2} で与えられます*1。
上記の f(f-1(B)) = B は反例があるので、間違った命題です。したがって証明はできません。間違った命題を証明できたなら、それは大変に困った事態です。
集合の内包的記法なら証明できる？
次のような形を集合の内包的記法と呼びます。
- {x∈X | P(x)}
この形において、変数xは集合X上を走るとします。P(x)は、xに関する何らかの条件を表す命題（ちゃんと書けば述語論理の論理式となる）です。一例を挙げると：
- {n∈N | nは2で割り切れる}
Nは自然数（非負整数）の全体のなので、これは非負の偶数全体を表します。
さて、f:X→Y の逆像と像を、集合の内包的記法で定義しましょう。
- f-1(B) = {x | f(x)∈B}
- f(A) = {f(x) | x∈A}
ちょっと雑ですが、xはX上の変数、yはY上の変数と決めれば、混乱はないでしょう。いま、A = f-1(B) と置いて、f(A) = f(f-1(B)) を計算してみます。左端は行番号で、後で参照しやすくするためのものです。
1: f(A)
2: = {f(x) | x∈A}
3: = {f(x) | x∈f-1(B)}
4: = {f(x) | f(x)∈B}
5: = {y | y∈B}
6: = B
等式変形のそれぞれのステップに対する根拠は：
- 1行から2行： fの像の定義
- 2行から3行： A = f-1(B) と事前に約束した
- 3行から4行： 逆像の定義より、x∈f-1(B) ⇔ f(x)∈B
- 4行から5行： f(x) = y と置く
- 5行から6行： B = {y | y∈B} は当たり前
結局、f(f-1(B)) = B が証明されたことになります。反例があったんだけどな？
何が問題なのか
前節の議論で採用した記法は色々と杜撰〈ずさん〉なところがありますが、一番の問題は次の書き方でしょう。
- f(A) = {f(x) | x∈A}
直感的には意味が分かりますが、像の定義として正確さに欠けます。像をちゃんと定義するには、存在限量子が必要です。次のようです。
- f(A) = {y | ∃x.(x∈A ∧ f(x) = y)}
変数x, yが走る範囲（変域、型）も明示すれば、
- f(A) = {y∈Y | ∃x∈X.(x∈A ∧ f(x) = y)}
この定義を使って、前節と同じ議論を途中までしてみます。
1: f(A)
2: = {y | ∃x.(x∈A ∧ f(x) = y)}
3: = {y | ∃x.(x∈f-1(B) ∧ f(x) = y)}
4: = {y | ∃x.(f(x)∈B ∧ f(x) = y)}
f(A) は {y | ∃x.(f(x)∈B ∧ f(x) = y)} と書けるのは分かりました。yはY上を走る変数ではありますが、自由な値を取れません。「f(x) = y となるxが在る」ような、そんなyしか考えないのです。f(A) = {f(x) | x∈A} という書き方は、存在命題による“縛り”が明白でないので、それを忘れがちなのです。その意味では好ましくない書き方です。
半分なら証明できる
f(f-1(B)) = B は反例があるので証明できません（証明できたらオカシイ！）が、f(f-1(B)) ⊆ B なら証明できます。集合の内包的記法はとても便利ですが、見通しが悪くなることもあるので、a∈{x | P(x)} ⇔ P(a) を使って、内包的記法を消去する方針にします。
言いたいこと、つまりターゲット命題は f(f-1(B)) ⊆ B ですが、これは次のように書けます（'⇒'は含意記号です）。
- y∈f(f-1(B)) ⇒ y∈B
ほんとは全称命題なので、全称限量子をちゃんと付ければ次のようです。
- ∀y∈Y.(y∈f(f-1(B)) ⇒ y∈B)
この命題を証明しなさい、という証明要求は、次の形です。「証明要求」という言葉や、'|-?'という記号については、“お膳立て”シリーズを読み返してください。
- |-? ∀y∈Y.(y∈f(f-1(B)) ⇒ y∈B)
さらに言えば、証明で使う予備知識や事前の約束（言葉や記号の定義）をΓ（大文字ガンマ）で表すなら、
- Γ |-? ∀y∈Y.(y∈f(f-1(B)) ⇒ y∈B)
これが言わんとしているところは、「あなたが知っている予備知識や事前の約束Γを使って、ターゲット命題 ∀y∈Y.(y∈f(f-1(B)) ⇒ y∈B) を証明しなさい」です。
f(f-1(B)) ⊆ B という包含関係は、「順序随伴性： ガロア接続の圏論」で述べた順序随伴に関する余単位不等式です。写像fの順像と逆像は順序随伴ペアになるのです。順序随伴の事例は、「証明の“お膳立て”のやり方 4： 随伴による集合差の定義」の例題としても扱っています。
[/補足]
“お膳立て”として証明要求を書き換えます。
Γ |-? ∀y∈Y.(y∈f(f-1(B)) ⇒ y∈B) -------------------------------------- Γ/ y:Y, |-? y∈f(f-1(B)) ⇒ y∈B -------------------------------------- Γ/ y:Y, y∈f(f-1(B)) |-? y∈B
予備知識や約束ごとΓのなかには、逆像と像の定義も入っています。それを使うと：
y∈f(f-1(B)) ⇔ ∃x∈X.(x∈f-1(B) ∧ f(x) = y) ⇔ ∃x∈X.(f(x)∈B ∧ f(x) = y)
証明要求の仮定を同値な命題で置き換えてもよいので、
- Γ/ y:Y, ∃x∈X.(f(x)∈B ∧ f(x) = y) |-? y∈B
“お膳立て”はここまでにして、実際の証明（フォワード・リーズニング）をします。
仮定に存在命題があるときの処方箋は、（少なくとも1つは）存在が保証された要素に名前を付けて利用することです。f(x)∈B ∧ f(x) = y であるようなXの要素を選び、aと命名します。当然ながら、そのaに関しては：
- f(a)∈B ∧ f(a) = y
f(a)∈B も f(a) = y も両方成立しているので、y∈B は成立します。これでターゲット命題 y∈ B が言えたので、証明要求を満たす〈satisfy | fulfill〉ことができました。すなわち、証明は終わりです。
仮定にある存在命題の使い方
前節の証明のキモは、仮定にある存在命題の使い方です。が、これは難しい。存在命題をうまく使えない、あるいは、使った証明に納得感を持てない人は多そうです。
パターン化するならば、次のようなブロック構造を使うのです。
…… ナニヤラカニヤラ ∃x.P(x) … この存在命題を使ってよいことになった +---------------------------------+ | P(a) であるaを選ぶ | …… aを使ってナニヤラカニヤラ | Q +---------------------------------+ Qを使ってよい
ボックス（ブロック）の内部がaを使った推論が行われる範囲です。Qはaを含まない命題です。aを含まないのでボックスの外に持ち出してもいいのです。前節の例ならば：
…… 仮定に ∃x∈X.(f(x)∈B ∧ f(x) = y) があるので ∃x∈X.(f(x)∈B ∧ f(x) = y) を使ってよい +---------------------------------+ | f(a)∈B ∧ f(a) = y であるaを選ぶ | f(a)∈B ∧ f(a) = y だ | だから | y∈B これはaを含まない +---------------------------------+ y∈B を使ってよい
仮定に存在命題があることは、ナニカが存在する状況下で考えていいよ、ってことです。そのナニカをaと呼び、しばらくはaを自由変数のように扱って議論をします。しかし、aは実際は縛りがある変数なので、自由変数のように扱うのはボックス内に限定して、aがボックスの外に漏れることを防ぎます。aを含まない命題はボックス外に持ち出してもいいもので、ボックス内のサブ証明の成果物と言えるでしょう。
追記： コメントへの応答 （2020-05-15）
Ryusei (id:mandel59) さんのコメントへの応答を本文内追記として書きます。本文だと見出しや文字修飾が使えますし、それと、はてなブログの仕様によりコメント欄だと下のほうが見えなくなるので。
何を問題視しているのか？（よくわからない）
Ryusei (id:mandel59) さんが、次の一文に注目しているのは間違いないでしょう。
檜山> f(A) = {f(x) | x∈A} という書き方は、存在命題による“縛り”が明白でないので、それを忘れがちなのです。その意味では好ましくない書き方です。
「好ましくない」という言葉を使っているので、批難してます。しかし批難の理由は、特定の状況下では（常にではない）間違いを引き起こしやすいからです。つまり、「誤操作しやすいUI〈ユーザーインターフェイス〉は好ましくない」と言っているようなものです。
Ryuseiさんは、「{f(x) | x∈A} という記法を弁護したい」とのこと。僕は弁護に耳を傾ける気はあります。が、誤操作しやすいUIに対して「注意深く操作すれば誤操作しない」と言われても何の解決にもなりません。「こういう理由でそのUIになった」と説明されても、誤操作しやすい事実は変わりません。
したがって僕は、「誤操作しやすい（間違いやすい）ぞ」という注意喚起を取り下げる気はありません。
おそらく（僕の推測ですが）、Ryuseiさんの弁護の主眼は別なところにあり、以下のことでしょう。
Ryuseiさん> 自分にとっては厳密に意味を定められている記法を、好ましくない書き方と主張されるのは政治的に困るので、反対を表明するのですが。
自分（Ryuseiさん）が正統で厳密だと信じている記法を、僕がないがしろにしたことに抗議したいのでしょう。
もしそうであるならば、「間違いやすい」から「正当性・厳密性」へと論点を移すべきですね。
{f(x) | x∈A} の正当性・厳密性
僕自身は、{f(x) | x∈A} の正当性・厳密性なんて考えたこともなく、それを話題にされても（唐突過ぎて）面食らってしまいます。正当性・厳密性の根拠は置換公理だという主張ですが、ますます意味不明で困惑します。（間違えにくい運用ルールを決めて、「この記法も積極的に使おう」というご提案なら賛成です。）
置換公理は、公理的集合論の専門家には必須のツールでしょうが、僕のような素人にはほぼ縁がないシロモノです。僕に限らず、線形代数／微積分／トポロジーなどの基礎素養として素朴集合論を使うだけの人が置換公理を知る機会はまずないでしょう。置換公理に出会わずに一生を過ごします。それは不要だからです。初等的な素朴集合論において置換公理の出番はありません。
僕は置換公理をそのように認識してますが、「実は、みんなも使ってるぜ」という事例があるのかも知れません。そこで、「いったいどんな場面で置換公理を使うのですか？」と質問しました。この質問への応答がありませんが、Ryuseiさんが質問に気付いてないか、もう飽きてしまったのかも知れません。
正当性・厳密性の根拠として、プロフェッショナルの道具や観点を持ち込むのはけっこうなことです。「なるほどそうなのか」という知見が得られます。しかしどうやら、Ryuseiさんは置換公理に対して何か誤解・誤認をしているように思われます。
置換公理
Ryuseiさん> {f(x) | x ∈ A} という記法は置換公理と対応していると考えられます。
考えられません。
Ryuseiさん> 記法{f(x) | x∈A}が置換公理に対応すると認めてしまえば、
認められません。
Ryuseiさん> その書き換えは、置換公理を使った集合の構成を分出公理を使った集合の構成に書き換えているのだ、というふうにも見ることができます。
見ることはできません。
と、いきなり否定的な書き方で気分を害されると思いますが、通常の（任意の）関数fの像の存在は、置換公理の使い所ではないし、そもそも置換公理から（任意の）fの像の存在は出ません。置換公理は、通常の任意の関数に適用可能な形はしていません。fが definable class function である前提です。
僕〈檜山〉は、初等的な素朴集合論に置換公理は不要と思ってます。僕のほうこそ誤解・誤認をしている、という可能性はあるでしょう。その場合は、ご指摘・ご教示ください。
