PAの実装としてのZFC
以前類似した質問をしており、また再質問になります、ご容赦ください。
１．PAのモデルには標準的なものと非標準的なものがあり、PA上の論理式では区別できないとよく目にします（だからこそ両方ともモデルといえる訳ですが）
しかし、これらのモデルもなんらかの実装で再帰的に定義して扱わないと形式の守備範囲でなくなってしまい、「PAでは」区別できないということが何を表しているか分からなくなってしまうと感じます。
そこでZFCを実装として使うものと理解していたのですがこれは正しい理解でしょうか。
つまり標準モデルNも非標準モデルも
実装としてZFCを使って、再帰的に別々のものとして個々に扱えると考えてよいのでしょうか（再帰的とは文字列間の関係として定義して、というような意味で使っています）。
また上の質問とは関係なくて申し訳ないのですが、もう一つ教えていただきたいことがあります。
２．算術の言語における理論Kに対して新たに、個体定数cを加え、次の可算無限個の論理式を公理として加える（sは後者関数）
c≠0、c≠s0、c≠ss0、c≠sss0、c≠ssss0・・・
そうして拡大した理論をK＋とする
などというのを良くみるのですが、
無限個の閉論理式を公理として加えるとは具体的にはどういう意味なのかということです。
理論にいわゆるシェーマというもので実質的に無限個の公理が含まれていることは認められるように感じるのですが、上の書き方では「・・・」の中に何が来るかが記述されてないように見えます（もちろんそれでも何が来るかは分かるのですが、論理式において見る側の類推に任せるというのは問題ではないでしょうか、しかし同時にどのような記述を採ったとしても見る側の類推に一切頼らないなどということはあり得ないのでは？とも感じるのです）。
例えば
c≠0、c≠φが公理であるとすればc≠sφも公理である
や
c≠0、 ∀n（c≠n→c≠s(n)）
などとしては意味がかわってしまうのでしょうか。（後者は強すぎる要請になってしまうのでしょうか）
懐疑論のような何を疑問に思ってるのかわかりにくい、そもそも疑問として成り立つのか怪しい質問と思いますが、
この方面に明るい方お時間に余裕があればよろしくお願いします。
![その他([技術者向] コンピューター) イメージ](https://gazo.okwave.jp/okwave/spn/images/related_qa/c205_2_thumbnail_img_sm.png)
