xとyの関係として，xがどのような値であってもy＝2となるというのは，定数関数です。yがどのような値であってもx＝3となるというのも，定数関数です。前者は「yはxの定数関数」，後者は「xはyの定数関数」です。
中学の数学で学ぶ関数について，一階述語論理の枠組みで，少し考えてみます。
発端はhttps://twitter.com/esumii/status/1055780029441892352のツイートなのですが，https://twitter.com/esumii/status/1055785005941645313のツイートを少し書き換え，
F1＝｛f｜［∀x∈D1 ∃y∈D2 (x,y)∈f］ ∧ ［∀x∈D1 ∀y1∈D2 ∀y2∈D2 (x,y1)∈f ∧ (x,y2)∈f ⇒ y1＝y2］｝
として，集合F1を定めます。「(x,y)∈f」を「y＝f(x)」に読み替えると，F1は，「yはxの関数である」と言えるようなもの全体の集合となります。
「∧」の左の部分，「∀x∈D1 ∃y∈D2 (x,y)∈f」については，「変数xのそれぞれの値に対し，変数yの値が（少なくとも1つ）存在する」を意味します。右の「∀x∈D1 ∀y1∈D2 ∀y2∈D2 (x,y1)∈f ∧ (x,y2)∈f ⇒ y1＝y2」は，「変数xのそれぞれの値に対し，対応する変数yの値は，2つ以上ない（たかだか1つ）」と解釈できます。これらを合わせると，「変数xの値を決めると，変数yの値がただ1つ決まる」ということです。
なおD1およびD2のDは，domainの頭文字で，訳すなら「定義域」ですが，中学数学の用語では「変域」であり，グラフをかくなどの際にはD1，D2とも実数全体の集合が想定されます*1。以下も実数を対象としますので，「∈D1」「∈D2」を取り除くと，
F1＝｛f｜［∀x ∃y (x,y)∈f］ ∧ ［∀x ∀y1 ∀y2 (x,y1)∈f ∧ (x,y2)∈f ⇒ y1＝y2］｝
と表せます。
同様にして，「yはxに比例する」という関数全体の集合F2を，以下のとおり表すことができます。
F2＝｛f｜［∀x ∃y (x,y)∈f］ ∧ ［∃a ∀x ∀y (x,y)∈f ⇒ y＝ax］｝
比例といったらy＝ax，なのですが，「∀x ∃y (x,y)∈f」がないと，例えばy＝ax（aは任意の定数）だけれどもx＝2のときだけyの値が定められていないような，xとyの関係について，比例と言えなくなってしまいます*2。「∃a ∀x ∀y (x,y)∈f ⇒ y＝ax」は「∀x ∀y1 ∀y2 (x,y1)∈f ∧ (x,y2)∈f ⇒ y1＝y2」を含む（［∃a ∀x ∀y (x,y)∈f ⇒ y＝ax］ ⇒ ［∀x ∀y1 ∀y2 (x,y1)∈f ∧ (x,y2)∈f ⇒ y1＝y2］を示せる）ので，F1でfに要請されている2番目の条件は，F2では明示していません。なお簡単のため，a＝0の場合（y＝0という定数関数）も，F2に属するものとしています。
一次関数，より正確には「yはxの一次関数である」という関数全体の集合F3は，次のようになります。
F3＝｛f｜［∀x ∃y (x,y)∈f］ ∧ ［∃a ∃b ∀x ∀y (x,y)∈f ⇒ y＝ax＋b］｝
同様にして，2次元平面上でグラフが直線になるような，xとyの対応付けを記述してみます。
F4＝｛f｜［∀x ∃y (x,y)∈f］ ∧ ［∃a ∃b ∃c ∀x ∀y (x,y)∈f ⇒ ax＋by＋c＝0 ］｝
このように書いてみましたが，これでは，y軸に平行な直線を表す，x＝h（hは任意の定数）が対象外となります。少し考えてみると，「∀x ∃y (x,y)∈f」を仮定したとき，「∃a ∃b ∀x ∀y (x,y)∈f ⇒ y＝ax＋b」と「∃a ∃b ∃c ∀x ∀y (x,y)∈f ⇒ ax＋by＋c＝0」は同値と分かります*3。ですのでF3＝F4です。
ここまでの集合F1からF4までは，「∀x ∃y (x,y)∈f」とあるとおり，任意の実数xに対し，xにfを適用したときの値が存在することを，要請しています。これを入れている限り，x＝hで表される，「xはyの定数関数」には対応できないということです。
https://twitter.com/takehikom/status/1056007347787620352では「定数関数を中学数学で教える必要はなさそう」と書きましたが，『中学総合的研究 数学 三訂版』*4ではp.243に，「x = h，y = kのグラフをかく」というのが入っていました。
*1:反比例を関数として考える場合，変域は，実数全体から0を除いた集合となります。
*2:x＝1のときy＝aです。しかしx＝2のときy＝2aではありません。これは，「xの値を2倍すると，yの値も2倍になる」という，比例の性質を満たしません。
*3:「［∃a ∃b ∃c ∀x ∀y (x,y)∈f ⇒ ax＋by＋c＝0 ］ ⇒ ［∃a ∃b ∀x ∀y (x,y)∈f ⇒ y＝ax＋b］」を示すには，異なるx1，x2において，ax1＋by1＋c＝0，ax2＋by2＋c＝0を満たすy1，y2が存在することを用います。x1≠x2で，2点(x1,y1)，(x2,y2)を通る直線の式は，y＝a'x＋b'の形で表せます。
